Embedded software is widely used in automotive applications, often in critical situations where reliability of the system is extremely important. Such systems often use model based development approaches. Model transformation is an important step in such scenarios. This includes generating code from models, transforming design models into analysis models, or transforming a model between variants of a formalism (such as variants of Statecharts). It becomes important to verify that the transformation was correct, and the transformed model or code preserved the semantics of the design model. In this paper, we will look at a technique called “goal-directed certification” that provides a pragmatic solution to the verification problem. We will see how we can use concepts of bisimulation to verify whether a certain transformation instance preserved certain properties. We will then extend this idea using weak bisimulation and semantic anchoring, to a more general class of transformations.
Towards Verification of Model Transformations Via Goal-Directed Certification
Automotive Software Workshop ; 2006 ; San Diego, CA, USA March 15, 2006 - March 17, 2006
2008-01-01
17 pages
Aufsatz/Kapitel (Buch)
Elektronische Ressource
Englisch
Behavior Preservation , Bisimulation , Weak Bisimulation , Semantic Anchoring Computer Science , Computer Communication Networks , Software Engineering/Programming and Operating Systems , Programming Techniques , Special Purpose and Application-Based Systems , Software Engineering , Computation by Abstract Devices
Towards Verification of Model Transformations Via Goal-Directed Certification
British Library Conference Proceedings | 2008
|A goal-directed transportation planning model
Elsevier | 1969
|A goal-directed transportation planning model
Elsevier | 1970
Boeing achieves major environmental certification goal
Emerald Group Publishing | 2009