In high-integrity systems, the focus of the development process is geared to assuring that the assertions made on the system are both correct (i.e., semantically sustainable) and feasible (i.e., true at run time). Some of those assertions take effect in the non-functional domain, that is, in how the system is realized and behaves in time, space and communication during execution; others in the functional domain, and thus concern what outputs the system produces for its inputs. In this paper, we address the problem of achieving correct specification and handling of non-functional attributes, with particular regard to the concurrent structure of the system, the safeness of the interaction protocols engaged in it, and the guarantee that its timing feasibility can be statically verified. Our approach is based on a Model-Driven Engineering methodology, in which correctness can be ensured by construction or verified at a high level of abstraction, while the runtime implementation structure and code are automatically generated. We employ the Ravenscar Computation Model (RCM) and focus, in particular, on aerospace applications, which impose stringent requirements on correctness properties. We discuss an algebraic formalization of our model based on graph theory which we use to prove safe termination in systems compliant with RCM, and show how to use the MAST+ static analyzer to verify the timing aspects. We finally illustrate the results of a prototype tool that was developed for evaluation by major industrial players in the European space industry.

Toward Correctness in the Specification and Handling of Non-Functional Attributes of High-Integrity Real-Time Embedded Systems / D., Cancila; Passerone, Roberto; T., Vardanega; M., Panunzio. - In: IEEE TRANSACTIONS ON INDUSTRIAL INFORMATICS. - ISSN 1551-3203. - STAMPA. - 6:2(2010), pp. 181-194. [10.1109/TII.2010.2043741]

Toward Correctness in the Specification and Handling of Non-Functional Attributes of High-Integrity Real-Time Embedded Systems

Passerone, Roberto;
2010-01-01

Abstract

In high-integrity systems, the focus of the development process is geared to assuring that the assertions made on the system are both correct (i.e., semantically sustainable) and feasible (i.e., true at run time). Some of those assertions take effect in the non-functional domain, that is, in how the system is realized and behaves in time, space and communication during execution; others in the functional domain, and thus concern what outputs the system produces for its inputs. In this paper, we address the problem of achieving correct specification and handling of non-functional attributes, with particular regard to the concurrent structure of the system, the safeness of the interaction protocols engaged in it, and the guarantee that its timing feasibility can be statically verified. Our approach is based on a Model-Driven Engineering methodology, in which correctness can be ensured by construction or verified at a high level of abstraction, while the runtime implementation structure and code are automatically generated. We employ the Ravenscar Computation Model (RCM) and focus, in particular, on aerospace applications, which impose stringent requirements on correctness properties. We discuss an algebraic formalization of our model based on graph theory which we use to prove safe termination in systems compliant with RCM, and show how to use the MAST+ static analyzer to verify the timing aspects. We finally illustrate the results of a prototype tool that was developed for evaluation by major industrial players in the European space industry.
2010
2
D., Cancila; Passerone, Roberto; T., Vardanega; M., Panunzio
Toward Correctness in the Specification and Handling of Non-Functional Attributes of High-Integrity Real-Time Embedded Systems / D., Cancila; Passerone, Roberto; T., Vardanega; M., Panunzio. - In: IEEE TRANSACTIONS ON INDUSTRIAL INFORMATICS. - ISSN 1551-3203. - STAMPA. - 6:2(2010), pp. 181-194. [10.1109/TII.2010.2043741]
File in questo prodotto:
File Dimensione Formato  
CPVP10TII.pdf

Solo gestori archivio

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 923.12 kB
Formato Adobe PDF
923.12 kB Adobe PDF   Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/85202
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 28
  • ???jsp.display-item.citation.isi??? 19
social impact