Rigorous Development of Embedded Systems Supported by Formal Tools

T. Szmuc, W. Szmuc (AGH Univ. of Science and Techn., Poland)

A rigorous approach to the development of embedded systems is proposed in the paper. The concept is based on introduction in parallel of formal modelling branch to the classical V-development method. SysML is used for the description of the developed components, and then these artefacts are translated into Coloured Petri Nets (CPN) blocks. The correctness of the CPN models is described using Temporal Logic and finally verified using model checking tools. The proposed concept enables detection of structural errors in early development stages. The paper describes the next steps of research in this area. Translations of remaining SysML diagrams are included, and the modelling-verification chain is described in more detail.