Multi-formalism Modelling and Model Transformation for the Design of Reactive Systems

摘要

This paper presents a development process based on modelling,rnsimulation, and code synthesis. The DCharts formalism,rna Statecharts variant with extensions, is used to model arnsmall application to demonstrate our approach: a traffic light.rnThe development of this system highlights the use of variousrnformalisms with appropriate supporting tools: AToM3, ArnTool for Multi-formalism and Meta-Modelling, is used as arnmulti-formalism visual modelling environment; SVM is thernsimulation engine used to experiment with prototype models;rnSCC is the code synthesizer that generates reusable sourcerncode in a variety of target languages. Transformation ontornthe Communicating Sequential Processes (CSP) formalismrnallows for model checking using the Failures DivergencesrnRefinement Checker (FDR2) model checker.We demonstraternhow using multiple formalisms as well as model transformationsrnduring the design process can drastically improve productivity,rnreliability and reusability.