Name
Abstract | ||
|---|---|---|
Large asynchronous systems composed from synchronous components (so called GALS--globally asynchronous, locally synchronous--systems) pose a challenge to formal verification. We present an approach which abstracts components with contracts capturing the behavior by a mixture of temporal logic formulas and non-deterministic state machines. Formal verification of global system properties is then done transforming a network of contracts to model checking tools such as Promela/SPIN or UPPAAL. Synchronous components are implemented in Scade, and contract validation is done using the Scade Design Verifier for formal verification. We also discuss first experiences from an ongoing industrial case study applying our approach. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-33678-2_25 | SAFECOMP |
Keywords | Field | DocType |
synchronous component,abstracts component,temporal logic formula,contract validation,scade design verifier,ongoing industrial case study,non-deterministic state machine,large asynchronous system,synchronous software component,global system property,formal verification,spin | Asynchronous communication,Model checking,Computer science,Finite-state machine,Verification,Promela,Component-based software engineering,Temporal logic,Reliability engineering,Formal verification | Conference |
Citations | PageRank | References |
4 | 0.39 | 26 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Henning Günther | 1 | 11 | 2.55 |
| Stefan Milius | 2 | 511 | 57.28 |
| Oliver Möller | 3 | 4 | 0.39 |