Istituto di Scienza e Tecnologie dell'Informazione     
Ferrari A., Fantechi A., Gnesi S. Lessons learnt from the adoption of formal model-based development. In: NFM 2012 - NASA Formal Methods Symposium. 4th International Symposium (Norfolk, VA, USA, 3-5 April 2012). Proceedings, pp. 24 - 38. Alwyn E. Goodloe, Suzette Person (eds.). (Lecture Notes in Computer Science, vol. 7226). Springer, 2012.
This paper reviews the experience of introducing formal mo- del-based design and code generation by means of the Simulink/Stateflow platform in the development process of a railway signalling manufacturer. Such company operates in a standard-regulated framework, for which the adoption of commercial, non qualified tools as part of the development activities poses hurdles from the verification and certification point of view. At this regard, three incremental intermediate goals have been defined, namely (1) identification of a safe-subset of the modelling language, (2) evidence of the behavioural conformance between the generated code and the modelled specification, and (3) integration of the modelling and code generation technologies within the process that is recommended by the regulations. These three issues have been addressed by progressively tuning the usage of the technologies across different projects. This paper summarizes the lesson learnt from this experience. In particular, it shows that formal modelling and code generation are actually powerful means to enhance product safety and cost effectiveness. Nevertheless, their adoption is not a straightforward step, and incremental adjustments and refinements are required in order to establish a formal model-based process.
URL: http://link.springer.com/chapter/10.1007%2F978-3-642-28891-3_5
DOI: 10.1007/978-3-642-28891-3_5
Subject Model-based development
Formal methods
Industrial experience
Code generation
Model checking
D.2.1 Requirements/Specifications
D.2.2 Design Tools and Techniques
D.2.4 Software/Program Verification

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional