REFINER Tool for Checking Property Preservation of Model Refinements

Organisation:	Technische Universiteit Eindhoven (THE NETHERLANDS)
Functionality:	Formal verification.
Tools used:	REFINER CADP (Construction and Analysis of Distributed Processes)
Period:	2013-2014
Description:	Model-driven software development entails creating implementations on a low level of abstraction from designs represented by models on a high level of abstraction. Implementation details, for example motivated by hardware restrictions, are added incrementally to these abstract models by means of refining model transformations. Usually, an implementation must satisfy a number of requirements that can be expressed as properties of the model that forms its design. Then, the transformations should preserve these properties. Model checking can help to determine whether this is the case, but verifying the properties from scratch for each new model along the development chain not only requires much time, but it is also likely to become unfeasible very quickly, as the related state space of a model tends to grow exponentially when applying a refinement. The REFINER tool implements an explicit-state model checking technique tailored for incremental refinement of models of concurrent systems. If the model that forms the initial design of such a system is relatively small, then at this stage, properties can still be verified using traditional techniques based on explicit state space exploration. When a refinement needs to be applied, then instead of the refined model, the technique analyses the formal semantics of the refinement, and determines whether application of the refinement is guaranteed to preserve a particular (safety, liveness, or fairness) property. This property-preservation checking is purely done by reasoning about the structures of Labelled Transition Systems (LTSs), which are used to express the semantics of both the models and the refinements. For a model, the semantics of each process in the model is expressed as an LTS, and the semantics of the complete concurrent system is expressed implicitly by a network of LTSs describing how these process LTSs interact. A refinement is formalised as a system of LTS transformation rules, where each rule has a left LTS pattern, describing what should be changed, and a right LTS pattern, describing what the result of the change should be. Furthermore, such a system can add to the interaction mechanism of the processes.
Conclusions:	The REFINER tool checks both semantics and property preservation by means of a single analysis technique, which enables the designer to refactor and restructure the models, as well as to check behaviour refinements. The technique is independent of the input and output models; it does not involve the state space of either of them, hence it usually works many orders of magnitude faster than repeated verification of the models through standard model checking, and it allows to build a repository of verified transformations. The tool integrates with action-based, explicit-state model checking toolsets such as CADP, which can be used to model concurrent systems in process algebras and automata, and to verify that the models satisfy functional properties.
Publications:	[Wijs-Engelen-13] Anton Wijs and Luc Engelen. "Efficient Property Preservation Checking of Model Refinements". Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2013, LNCS vol. 7795, pages 565-579. Springer Verlag, 2013. Available on-line at: http://dx.doi.org/10.1007/978-3-642-36742-7_41 or from the CADP Web site in PDF or PostScript [Wijs-14] Anton Wijs. "Define, Verify, Refine: Correct Composition and Transformation of Concurrent System Semantics". Proceedings of the 10th International Symposium on Formal Aspects of Component Software FACS'2013 (Nanchang, China), LNCS vol. 8348, pages 348-368. Springer Verlag, 2014. Available on-line at: http://dx.doi.org/10.1007/978-3-319-07602-7_21 or from the CADP Web site in PDF or PostScript [Wijs-Engelen-14] Anton Wijs and Luc Engelen. "REFINER: Towards Formal Verification of Model Transformations". Proceedings of the NASA Formal Methods 6th International Symposium NFM'2014 (Houston, TX, USA), LNCS vol. 8430, pages 258-263. Springer Verlag, 2014. Available on-line at: http://dx.doi.org/10.1007/978-3-319-06200-6_21 or from the CADP Web site in PDF or PostScript [DePutter-Wijs-17] Sander de Putter and Anton Wijs. "A Formal Verification Technique for Behavioural Model-to-model Transformations". Formal Aspects of Computing 30 (1), pages 3-43, January 2018. Available on-line at: https://link.springer.com/article/10.1007/s00165-017-0437-z or from the CADP Web site in PDF or PostScript
Contact:	Anton Wijs Technische Universiteit Eindhoven MetaForum 6.077 Software Engineering and Technology Faculteit Informatica Den Dolech 2 5612 AZ Eindhoven THE NETHERLANDS Tel: +49 (0)241 80 21206 Email: A.J.Wijs@tue.nl
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page