Formal Requirement Models for Automotive Embedded Systems
John R. Eriksson · KTH Publication Database DiVA (KTH Royal Institute of Technology) · 2016
Embedded systems are a crucial part of modern vehicles today and are used widely by the automotive industry to control safety-critical functions. To verify that the software will work correctly, formal verification can be used to prove that the code will always behave correctly according to some specification. This report will look into how to formulate the specification in such a way that it is easy to use, consistent and can be used efficiently for code verification. Two different models are looked into in the report, and applied to real automotive embedded code. From this, conclusions are made about the different models.