Pierre-Loïc Garoche
- Published in print:
- 2019
- Published Online:
- January 2020
- ISBN:
- 9780691181301
- eISBN:
- 9780691189581
- Item type:
- chapter
- Publisher:
- Princeton University Press
- DOI:
- 10.23943/princeton/9780691181301.003.0001
- Subject:
- Mathematics, Applied Mathematics
This chapter looks at the current state of physical systems controlled by an onboard computer. Typically this covers transportation systems such as cars, aircraft, railway systems, space systems, or ...
More
This chapter looks at the current state of physical systems controlled by an onboard computer. Typically this covers transportation systems such as cars, aircraft, railway systems, space systems, or even medical devices, all of them either for the expected harmfulness for people, or for the huge cost associated with their failure. The chapter shows how the increase of computer use in those systems has led to huge benefits, but also an exponential growth in complexity. Furthermore, the drawback of this massive introduction of computers to control systems is the lack of predictability for both computer and software. This chapter shows how the aerospace industry, and more generally critical embedded systems industries, is now facing a huge increase in the software size in their systems. This in turn creates a greater system complexity increase because of safety or performance objectives. Moreover, this complexity leads to the need to integrate even more advanced algorithms to sustain autonomy and energy efficiency.Less
This chapter looks at the current state of physical systems controlled by an onboard computer. Typically this covers transportation systems such as cars, aircraft, railway systems, space systems, or even medical devices, all of them either for the expected harmfulness for people, or for the huge cost associated with their failure. The chapter shows how the increase of computer use in those systems has led to huge benefits, but also an exponential growth in complexity. Furthermore, the drawback of this massive introduction of computers to control systems is the lack of predictability for both computer and software. This chapter shows how the aerospace industry, and more generally critical embedded systems industries, is now facing a huge increase in the software size in their systems. This in turn creates a greater system complexity increase because of safety or performance objectives. Moreover, this complexity leads to the need to integrate even more advanced algorithms to sustain autonomy and energy efficiency.
Pierre-Loïc Garoche
- Published in print:
- 2019
- Published Online:
- January 2020
- ISBN:
- 9780691181301
- eISBN:
- 9780691189581
- Item type:
- chapter
- Publisher:
- Princeton University Press
- DOI:
- 10.23943/princeton/9780691181301.003.0002
- Subject:
- Mathematics, Applied Mathematics
This chapter gives a brief overview of some formal methods and their use in the context of critical embedded systems development. While testing is a common practice for a lot of engineers as a way to ...
More
This chapter gives a brief overview of some formal methods and their use in the context of critical embedded systems development. While testing is a common practice for a lot of engineers as a way to evaluate whether the program they developed fulfills its needs, formal methods are less known and may require a little introduction to the non-expert. This chapter thus serves as a reasonable introduction to the control expert engineer. It first defines the semantics of programs: their basic properties and their meaning. Then, the chapter outlines different formal verifications and explains how they reason on the program artifact. A last part addresses the soundness of the analyses with respect to the actual semantics.Less
This chapter gives a brief overview of some formal methods and their use in the context of critical embedded systems development. While testing is a common practice for a lot of engineers as a way to evaluate whether the program they developed fulfills its needs, formal methods are less known and may require a little introduction to the non-expert. This chapter thus serves as a reasonable introduction to the control expert engineer. It first defines the semantics of programs: their basic properties and their meaning. Then, the chapter outlines different formal verifications and explains how they reason on the program artifact. A last part addresses the soundness of the analyses with respect to the actual semantics.
