A case study in UML model-based dynamic validation: the Ariane-5 launcher software

Content Provider	Semantic Scholar
Author	Ober, Iulian Graf, Susanne Lesens, David
Copyright Year	2005
Abstract	The aim of this paper is to show the usefulness of IFx, an extension of the IF validation toolset for timed and complex systems, for the validation of designs represented using the UML profile defined in the IST Omega project. This demonstration is done on hand of a realistic case study, a model of the Ariane-5 launcher software. In this case study, we do not address the correctness of the control algorithms, which may be specified as global transactions and validated with the help of synchronous tools such as Scade. We are rather interested in the expression of non functional properties which allow to guarantee the correctness of this transactional view and their validation on a model of the distributed architecture on which the system is deployed. We provide examples of complex properties and their expression by UML observer state-machines, where special attention is paid to the modelling of properties expressing time constraints and schedulability. Also, on hand of this example, a validation methodology is demonstrated which has been experimented already in a number of real-life examples. This case study is representative for systems in the aerospace domain concerning the nature and complexity of the handled verification problems. Code generation form the developed software model was not part of this case study, but the obtained model is such that it can be refined into a complete model including also all functional aspects from which existing code generation techniques may be applied. ? This work has been partially financed by the OMEGA IST project
File Format	PDF HTM / HTML
Alternate Webpage(s)	http://www-verimag.imag.fr/~graf/ARTIST-summerschool/Omega-Ariane-draft.pdf
Language	English
Access Restriction	Open
Content Type	Text
Resource Type	Article