Representing Behavioural Models with Rich Control Structures in SMT-LIB
MetadataShow full item record
We motivate and present a proposal for how to represent extended finite state machine behavioural models with rich hierarchical states and compositional control structures (e.g., the Statecharts family) in SMT-LIB. Our goal with such a representation is to facilitate automated deductive reasoning on such models, which can exploit the structure found in the control structures. We present a novel method that combines deep and shallow encoding techniques to describe models that have both rich control structures and rich datatypes. Our representation permits varying semantics to be chosen for the control structures recognizing the rich variety of semantics that exist for the family of extended finite state machine languages. We hope that discussion of these representation issues will facilitate model sharing for investigation of analysis techniques.
Cite this version of the work
Nancy A. Day, Amirhossein Vakili (2015). Representing Behavioural Models with Rich Control Structures in SMT-LIB. UWSpace. http://hdl.handle.net/10012/16038