TRANSFORMAL is a project of the Systems Engineering Group of Mechanical Engineering and the Formal Methods Group of Mathematics and Computer Science, both at TU/e, studying the model based design of systems using models at different levels of abstraction. The TRANSFORMAL project is part of a larger European project named MULTIFORM.
The process of designing a functioning system includes several steps which are distinguished from one another by the level of abstraction of the models used. We start from an abstract model, and try to solve our problem at that level. If the abstract model of the system satisfies our high-level criteria, then we add more detail and check whether the thus obtained system still satisfies our high-level requirements, and in addition our new lower-level requirements. We validate the model of the system, and in case design faults are found we go back to a higher level of abstraction and correct the faults either through re-designing or by using a different refinement. Eventually, a prototype is built, tested, and validated. The procedure above can be called model based design through step-wise model refinement.
The described approach requires the development of formalisms, tools and methods for systematic reasoning about models on different abstraction levels. More specifically, we need proof techniques for showing that a property which holds for an abstract model will still hold after adding additional details. For example, one may want to know if an abstract control algorithm (i.e. a simple feedback law) will function correctly and have good performance when implemented on a real-time operating system. The analysis of functional correctness in a timed environment and the performance analysis require different levels of detail (i.e. the actual program or the sampling and quantization characteristics) that are not included in the abstract description of the control algorithm. Furthermore, analysis of the different refinements may require different analysis methods, which are unlikely to be provided all in one toolset.
The TRANSFORMAL project addresses this problem by developing suitable definitions for step-wise refinement of Chi models, in combination with a toolset to support such refinement. The advantage of Chi in particular, in this case, is that it already supports a wide range of modelling concepts (it supports the syntax for discrete, hybrid, timed and stochastic features). Thus, the refinements do not need to span multiple languages. Finally, the development of interchange formats within the MULTIFORM project will ensure that refinement of Chi models in languages such as Uppaal, PHAVer and Modelica becomes possible.
Three types of refinement are highly relevant in current industrial practice. The first one is especially relevant from a functional software-development viewpoint, while the last two are especially relevant in the context of performance of embedded systems.
Although the application of the above refinements covers a variety of application areas, there are many commonalities in their development. For each of the refinements, the following questions need to be addressed:
Furthermore, within the MULTIFORM project, tools will be implemented that carry out the refinement of models in an intuitive and user-friendly way.
The Chi formalism combines ease of modeling with a straightforward, formal semantics. Ease of modeling is ensured by several concepts, such as different classes of variables, urgent and non-urgent actions and communication channels, and several other user-friendly syntactic extensions. Chi is suited to modeling, simulation, and verification of (timed) discrete-event systems, continuous-time systems with algebraic constraints, and combined discrete-event / continuous-time systems. It is especially suited to the specification and analysis of complex systems since it supports process re-use, encapsulation, hierarchical and/or modular composition of processes, and different interaction mechanisms such as handshake synchronization, synchronous communication and actions, and shared variables. Chi has been widely used in industrial projects and offers extensive tool support.
For application of the theory, techniques, and tools for refinement, many opportunities are available in our network of industrial partners in the Netherlands:
J.C.M. Baeten, D.A. van Beek, P.J.L. Cuijpers, M.A. Reniers, J.E. Rooda, R.R.H. Schiffelers, R.J.M. Theunissen. Model-based engineering of embedded systems using the hybrid process algebra Chi, Electronic Notes in Theoretical Computer Science, accepted.
D.A. van Beek, J.E. Rooda, R.R.H. Schiffelers, K.L. Man, M.A. Reniers. Relating hybrid Chi to other formalisms. Electronic Notes in Theoretical Computer Science, vol. 191, 85-113, 2007.
D.A. van Beek, K.L. Man, M.A. Reniers, J.E. Rooda, R.R.H. Schiffelers. Syntax and Consistent Equation Semantics of Hybrid Chi. Journal of Logic and Algebraic Programming, special issue on hybrid systems, vol. 68, no. 1-2, 129-210, 2006.
D.A. van Beek and J.E. Rooda. Languages and applications in hybrid modelling and simulation: Positioning of Chi. Control Engineering Practice, vol. 8, no. 1, 81-91, 2000.
J.C.M. Baeten, D.A. van Beek, J.E. Rooda. Process algebra. In Handbook on Dynamic System Modeling, Editors: Paul A. Fishwick, 19-1 – 19-21, Chapman & Hall/CRC, Book Chapter, ISBN 978-1-58488-565-8, 2007.
K.L. Man and R.R.H. Schiffelers. Formal specification and analysis of hybrid systems. Ph.D. thesis, Eindhoven University of Technology, 2006.
D.A. van Beek, M.A. Reniers, R.R.H. Schiffelers, J.E. Rooda. Concrete syntax and semantics of the compositional interchange format for hybrid systems. In Proc. 17th IFAC World Congress, Seoul, Korea, 2008, accepted.
D.A. van Beek, A.T. Hofkamp, M.A. Reniers, J.E. Rooda, R.R.H. Schiffelers. Co-simulation of Chi and Simulink models. In Proc. 6th EUROSIM congress on Modelling and Simulation, Ljubljana, Slovenia, CD-ROM, 2007.
D.A. van Beek, M.A. Reniers, R.R.H. Schiffelers, J.E. Rooda. Foundations of a compositional interchange format for hybrid systems. In 10th International Conference on Hybrid Systems: Computation and Control, Editors: Alberto Bemporad, Antonio Bicchi, and Giorgio Buttazzo, Pisa, Italy, 587-600, 2007.
D.A. van Beek, K.L. Man, M.A. Reniers, J.E. Rooda, R.R.H. Schiffelers. Deriving Simulators for Hybrid Chi Models. In Proc. Computer Aided Control System Design, Munich, 2006.
D.A. van Beek, K.L. Man, M.A. Reniers, J.E. Rooda, R.R.H. Schiffelers. Formal verification of Chi models using PHAVer. In Proc. MathMod 2006, Editors: I. Troch and F. Breitenecker, Vienna, Austria, CD-ROM, 2006.
E.M. Bortnik, D.A. van Beek, J.M. van de Mortel-Fronczak, J.E. Rooda. Verification of timed Chi models using Uppaal. In Proc. 2nd International Conference on Informatics in Control, Robotics and Automation, Editors: J. Filipe, J.A. Cetto, J.-L. Ferrier, Barcelona, Spain, pp. 486-492, 2005.
D.A. van Beek, M.A. Reniers, J.E. Rooda, R.R.H. Schiffelers. Revised hybrid system interchange format. HYCON Deliverable D3.6.3. HYCON network of excellence, 2007.