Specification and Validation of Embedded Systems using LUSTRE and ARGOS. Case Study: The Automatic Headlight Leveling System

In thisarticle, the design, modeling and validation of embedded systemsis examined. There exist commercial tools for the developmentof control- or data-flow dominated systems, e.g.STATEMATE for control dominated systems and MATLAB for data-flowdominated systems, but there are problems to describe mixed systems.The system is split in a control and a transformation part. Thecontrol part is described with the graphical language ARGOS,the transformation part with the data-flow language LUSTRE. Integrationis done based on their common synchronous architecture. The designprocess is shown in a case study on an industrial application,the automatic headlight leveling system. A validation strategyaccording to the separation of the system is shown. Safety propertiesof the control part are proved with model checking, functionalcorrectness is shown in two steps by simulation and hardwarein the loop simulation.