Contributo in atti di convegno, 2012, ENG, 10.1007/978-3-642-28891-3_5

Lessons learnt from the adoption of formal model-based development.

Ferrari A., Fantechi A., Gnesi S.

CNR-ISTI, Pisa, Italy; DSI, Universita degli Studi di Firenze, Firenze, ITALY

This paper reviews the experience of introducing formal model-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.

NASA Formal Methods Symposium. 4th International Symposium, pp. 24–36, Norfolk, VA, USA, 3-5 April 2012

Keywords

Development activity; Development process; Formal modelling;

CNR authors

Gnesi Stefania, Ferrari Alessio

CNR institutes

ISTI – Istituto di scienza e tecnologie dell'informazione "Alessandro Faedo"

ID: 220735

Year: 2012

Type: Contributo in atti di convegno

Creation: 2013-05-31 09:38:03.000

Last update: 2023-03-08 13:35:32.000

External IDs

CNR OAI-PMH: oai:it.cnr:prodotti:220735

DOI: 10.1007/978-3-642-28891-3_5

Scopus: 2-s2.0-84859459699

PUMA: cnr.isti/2012-A2-047