A model review is a validation technique aimed at determining if a model is of sufficient quality and allows defects to be identified early in the system development, reducing the cost of fixing them. In this paper we propose a technique to perform automatic review of Abstract State Machine (ASM) formal specifications. We first detect a family of typical vulnerabilities and defects a developer can introduce during the modeling activity using the ASMs and we express such faults as the violation of meta-properties that guarantee certain quality attributes of the specification. These meta-properties are then mapped to temporal logic formulas and model checked for their violation. As a proof of concept, we also report the result of applying this ASM review process to several specifications.
Automatic review of Abstract State Machines by meta-property verification / P. Arcaini, A. Gargantini, E. Riccobene - In: Proceedings of the Second NASA formal methods symposium / [a cura di] C. Muñoz. - Hanover : NASA, 2010. - pp. 4-13 (( Intervento presentato al 2. convegno NASA Formal Methods Symposium tenutosi a Washington nel 2010.
Automatic review of Abstract State Machines by meta-property verification
P. ArcainiPrimo
;E. RiccobeneUltimo
2010
Abstract
A model review is a validation technique aimed at determining if a model is of sufficient quality and allows defects to be identified early in the system development, reducing the cost of fixing them. In this paper we propose a technique to perform automatic review of Abstract State Machine (ASM) formal specifications. We first detect a family of typical vulnerabilities and defects a developer can introduce during the modeling activity using the ASMs and we express such faults as the violation of meta-properties that guarantee certain quality attributes of the specification. These meta-properties are then mapped to temporal logic formulas and model checked for their violation. As a proof of concept, we also report the result of applying this ASM review process to several specifications.File | Dimensione | Formato | |
---|---|---|---|
NASA-CP-2010-216215.pdf
accesso aperto
Tipologia:
Pre-print (manoscritto inviato all'editore)
Dimensione
5.45 MB
Formato
Adobe PDF
|
5.45 MB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.