Abstract—We present an approach for integration of formal methods within an industrial SW process, illustrating results obtained in a real scenario subject to Military Standard 498 (MIL-STD-498). On the one hand, the formal nucleus of preemptive Time Petri Nets (pTPNs) is used to support design and verification activities of the development process; on the other hand, the UML (Unified Modeling Language) profile for MARTE (Modeling and Analysis of Real-Time and Embedded systems) is adopted to manage the documentation process prescribed by MIL-STD-498. The two cores are integrated by providing guidance for translation of UML-MARTE specifications into equivalent pTPN models, with specific reference to concurrency control and synchronization mechanisms. This permits to attain a smooth transition from the standard artifacts of MIL-STD-498 to pTPN models and analyses, facilitating deployment of the formal core of pTPNs with a limited impact on the industrial practice. The experience proves practical feasibility and effectiveness of the approach, comprising a step towards industrial applicability of formal methods and practices.
Combining UML-MARTE and preemptive Time Petri Nets: An Industrial Case Study / I. Bicchierai;G. Bucci;L. Carnevali;E. Vicario. - In: IEEE TRANSACTIONS ON INDUSTRIAL INFORMATICS. - ISSN 1551-3203. - STAMPA. - 9:(2013), pp. 1806-1818. [10.1109/TII.2012.2205399]
Combining UML-MARTE and preemptive Time Petri Nets: An Industrial Case Study
BICCHIERAI, IRENE;BUCCI, GIACOMO;CARNEVALI, LAURA;VICARIO, ENRICO
2013
Abstract
Abstract—We present an approach for integration of formal methods within an industrial SW process, illustrating results obtained in a real scenario subject to Military Standard 498 (MIL-STD-498). On the one hand, the formal nucleus of preemptive Time Petri Nets (pTPNs) is used to support design and verification activities of the development process; on the other hand, the UML (Unified Modeling Language) profile for MARTE (Modeling and Analysis of Real-Time and Embedded systems) is adopted to manage the documentation process prescribed by MIL-STD-498. The two cores are integrated by providing guidance for translation of UML-MARTE specifications into equivalent pTPN models, with specific reference to concurrency control and synchronization mechanisms. This permits to attain a smooth transition from the standard artifacts of MIL-STD-498 to pTPN models and analyses, facilitating deployment of the formal core of pTPNs with a limited impact on the industrial practice. The experience proves practical feasibility and effectiveness of the approach, comprising a step towards industrial applicability of formal methods and practices.File | Dimensione | Formato | |
---|---|---|---|
TII13.pdf
Accesso chiuso
Tipologia:
Pdf editoriale (Version of record)
Licenza:
Tutti i diritti riservati
Dimensione
2.11 MB
Formato
Adobe PDF
|
2.11 MB | Adobe PDF | Richiedi una copia |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.