Abstract
Live Sequence Charts (LSCs) are an established visual formalism for requirements in formal, model-based development, in particular aiming at formal verification of the model. The model-checking problem for LSCs is principally long solved as each LSC has an equivalent LTL formula, but even for moderate sized LSCs the formulae grow prohibitively large. In this paper we elaborate on practically relevant sub-classes of LSCs, namely bonded and time bounded, which don't require the full power of LTL model-checking. For bonded LSCs, a combination of observer automaton and fixed small liveness property and for additionally time bounded LSCs reachability checking is sufficient. © Springer-Verlag Berlin Heidelberg 2006.
Cite
CITATION STYLE
Klose, J., Toben, T., Westphal, B., & Wittke, H. (2006). Check it out: On the efficient formal verification of live sequence charts. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4144 LNCS, pp. 219–233). Springer Verlag. https://doi.org/10.1007/11817963_22
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
