We present CoMA (Conformance Monitoring by Abstract State Machines), a specification-based approach and its supporting tool for runtime monitoring of Java software. Based on the information obtained from code execution and model simulation, the conformance of the concrete implementation is checked with respect to its formal specification given in terms of Abstract State Machines. At runtime, undesirable behaviors of the implementation, as well as incorrect specifications of the system behavior are recognized. The technique we propose makes use of Java annotations, which link the concrete implementation to its formal model, without enriching the code with behavioral information contained only in the abstract specification. The approach fosters the separation between implementation and specification, and allows the reuse of specifications for other purposes (formal verification, simulation, model-based testing, etc.).
CoMA : Conformance Monitoring of Java Programs by Abstract State Machines / P. Arcaini, A. Gargantini, E. Riccobene - In: Runtime verification : Second International Conference, RV 2011, San Francisco, CA, USA, September 27-30, 2011, revised selected papers / [a cura di] K. Sen, S. Khurshid. - New York : Springer, 2012. - ISBN 9783642298592. - pp. 223-238 (( Intervento presentato al 2. convegno Runtime verification tenutosi a San Francisco nel 2011 [10.1007/978-3-642-29860-8_17].
CoMA : Conformance Monitoring of Java Programs by Abstract State Machines
P. Arcaini;E. Riccobene
2012
Abstract
We present CoMA (Conformance Monitoring by Abstract State Machines), a specification-based approach and its supporting tool for runtime monitoring of Java software. Based on the information obtained from code execution and model simulation, the conformance of the concrete implementation is checked with respect to its formal specification given in terms of Abstract State Machines. At runtime, undesirable behaviors of the implementation, as well as incorrect specifications of the system behavior are recognized. The technique we propose makes use of Java annotations, which link the concrete implementation to its formal model, without enriching the code with behavioral information contained only in the abstract specification. The approach fosters the separation between implementation and specification, and allows the reuse of specifications for other purposes (formal verification, simulation, model-based testing, etc.).File | Dimensione | Formato | |
---|---|---|---|
rv2011_cr.pdf
accesso aperto
Tipologia:
Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione
374.2 kB
Formato
Adobe PDF
|
374.2 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.