Improving formal analysis of state machines with particular emphasis on and-cross transitions

• Published in: Computer languages, systems & structures systems & structures, 2018-12, Vol.54, p.544-585
• Main Authors: Adesina, Opeyemi O., Lethbridge, Timothy C., Somé, Stéphane S., Abdelzad, Vahdat, Belle, Alvine Boaye
• Format: Article
• Language: English
• Subjects: Cross transitions; Model checking; Model-driven engineering; Software quality assurance; State diagrams; Umple
• ISSN: 1477-8424; 1873-6866
• DOI: 10.1016/j.cl.2017.12.001

•And-cross transitions are a useful abstraction that can make some constructs easier to specify for the modeler.•They can be transformed to and from alternative modeling solutions that require a greater number of transitions.•With fewer transitions, the time taken and memory required to certify a model to be deterministic using formal methods can be much reduced compared to other approaches. This is related to the time and memory required to compute the set of pairs of potentially conflicting transitions. In this paper, we present an approach to formally encode state machines expressed in Umple for symbolic verification. We illustrate this with a real-world modeling example that encodes and analyzes and-cross transitions. This paper discusses a formal description of our approach to represent state machine systems under analysis (SSUAs); a systematic approach to certifying that SSUAs are deterministic; and an evaluation of performance (memory usage and execution time) on the case study. We describe a formalization of state machines in Umple that enables their translation to model checking tools and also to code that is consistent with this. We present three alternative modeling solutions for a sample problem and a solution based on the use of and-cross transitions. State machine models corresponding to these solutions are represented in Umple, a model-oriented programming language. These are automatically transformed to SMV, the input language of the nuXmv (or NuSMV) model checker. By cleanly separating concerns, we systematically integrate components of hierarchical state systems as opposed to the traditional flattening approach, yet manage the complexity introduced by concurrency and and-crossing. We then compose and verify a set of requirements (e.g., correctness, safety, liveliness, etc.) on the resulting systems of all the modeling approaches to empirically compare the different modeling alternatives with the use of and-cross transitions. We can encode and formally analyse complex state machines with and-cross transition(s). We observed a large reduction in the number of required transitions for encoding the SSUA, as opposed to the alternative approaches. We asserted that solutions derived from the approaches are identical behavior-wise even though each approach models the SSUA differently. Each of the approaches yielded the same result for potentially conflicting pairs which is a false positive (i.e., the SSUAs are deterministic). We observe that each