DocumentCode :
637326
Title :
Trace based reachability verification for statecharts
Author :
Madhukar, Kumar ; Metta, Ravindra ; Shrotri, Ulka ; Venkatesh, R.
Author_Institution :
TRDDC, Tata Consultancy Services, Pune, India
fYear :
2013
fDate :
25-25 May 2013
Firstpage :
22
Lastpage :
28
Abstract :
Statecharts are widely used to model the behavior of reactive systems. While this visual formalism makes modeling easier, the state of the art in verification of statechart specifications is far from satisfactory due to the state explosion problem. We present History ion, a trace-based verification technique to address this problem. Given a set of traces in a statechart model, the model is abstracted to contain at most three states per statechart: current, history and future. A path to a desired state in the abstract model is a sketch of a potential path to that state in the original model. We follow an incremental concretization procedure to extend the sketch to a complete path in the original model. This paper presents our technique. Our experiments suggest that the technique scales to large industry models.
Keywords :
formal specification; formal verification; reachability analysis; abstract model; history ion; incremental concretization procedure; industry models; reactive systems; state explosion problem; statechart specifications; statecharts; trace based reachability verification; trace-based verification technique; visual formalism; Abstracts; Concrete; Data models; Explosions; History; Vehicle dynamics;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Formal Methods in Software Engineering (FormaliSE), 2013 1st FME Workshop on
Conference_Location :
San Francisco, CA
Type :
conf
DOI :
10.1109/FormaliSE.2013.6612273
Filename :
6612273
Link To Document :
بازگشت