Name
Title | ||
|---|---|---|
Towards automatic generation of formal specifications to validate and verify reliable distributed systems: a method exemplified by an industrial case study |
Abstract | ||
|---|---|---|
The validation and verification of reliable systems is a difficult and complex task, mainly for two reasons: First, it is difficult to precisely state which formal properties a system needs to fulfil to be of high quality. Second, it is complex to automatically verify such properties, due to the size of the analysis state space which grows exponentially with the number of components. We tackle these problems by a tool-supported method which embeds application functionality in building blocks that use UML activities to describe their internal behaviour. To describe their externally visible behaviour, we use a combination of complementary interface contracts, so-called ESMs and EESMs. In this paper, we present an extension of the interface contracts, External Reliability Contracts (ERCs), that capture failure behaviour. This separation of different behavioural aspects in separate descriptions facilitates a two-step analysis, in which the first step is completely automated and the second step is facilitated by an automatic translation of the models to the input syntax of the model checker TLC. Further, the cascade of contracts is used to separate the work of domain and reliability experts. The concepts are proposed with the background of a real industry case, and we demonstrate how the use of interface contracts leads to significantly smaller state spaces in the analysis. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1145/2047862.2047888 | GPCE |
Keywords | Field | DocType |
externally visible behaviour,formal specification,separate description,internal behaviour,capture failure behaviour,complex task,interface contract,towards automatic generation,two-step analysis,smaller state space,complementary interface contract,industrial case study,analysis state space,model driven engineering,state space,distributed system,model checking,fault tolerance,fault tolerant,validation and verification | Model checking,Verification and validation,Unified Modeling Language,Model-driven architecture,Computer science,Formal specification,Fault tolerance,State space,Syntax,Distributed computing | Conference |
Volume | Issue | ISSN |
47 | 3 | 0362-1340 |
Citations | PageRank | References |
5 | 0.43 | 23 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Vidar Slåtten | 1 | 61 | 4.65 |
| Frank Alexander Kraemer | 2 | 262 | 21.13 |
| Peter Herrmann | 3 | 153 | 12.37 |