Name
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. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/11817963_22 | CAV |
Keywords | Field | DocType |
efficient formal verification,established visual formalism,live sequence charts,ltl model-checking,fixed small liveness property,live sequence chart,full power,equivalent ltl formula,model-checking problem,lscs reachability checking,model-based development,formal verification,model checking | Kripke structure,Model checking,Computer science,Algorithm,Theoretical computer science,Formal specification,Reachability,Temporal logic,Liveness,Bounded function,Formal verification | Conference |
Volume | ISSN | ISBN |
4144 | 0302-9743 | 3-540-37406-X |
Citations | PageRank | References |
24 | 1.04 | 14 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jochen Klose | 1 | 151 | 10.10 |
| Tobe Toben | 2 | 95 | 8.28 |
| Bernd Westphal | 3 | 65 | 4.39 |
| Hartmut Wittke | 4 | 114 | 6.58 |