Name
Abstract | ||
|---|---|---|
Given a global specification contract and a system described by a composition of contracts, system verification reduces to checking that the composite contract refines the specification contract, i.e. that any implementation of the composite contract implements the specification contract and is able to operate in any environment admitted by it. Contracts are captured using high-level declarative languages, for example, linear temporal logic (LTL). In this case, refinement checking reduces to an LTL satisfiability checking problem, which can be very expensive to solve for large composite contracts. This paper proposes a scalable refinement checking approach that relies on a library of contracts and local refinement assertions. We propose an algorithm that, given such a library, breaks down the refinement checking problem into multiple successive refinement checks, each of smaller scale. We illustrate the benefits of the approach on an industrial case study of an aircraft electric power system, with up to two orders of magnitude improvement in terms of execution time. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.7873/DATE.2014.167 | Design, Automation and Test in Europe Conference and Exhibition |
Keywords | Field | DocType |
high level languages,logic design,refinement calculus,temporal logic,LTL satisfiability checking problem,aircraft electric power system,composite contract,contract-based design,global specification contract,high-level declarative languages,library-based scalable refinement checking,linear temporal logic,multiple successive refinement checks,scalable refinement checking approach | Logic synthesis,Programming language,Model checking,Refinement calculus,Computer science,Satisfiability,Real-time computing,Linear temporal logic,High-level programming language,Temporal logic,Scalability | Conference |
ISSN | Citations | PageRank |
1530-1591 | 9 | 0.49 |
References | Authors | |
9 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Antonio Iannopollo | 1 | 14 | 2.59 |
| Pierluigi Nuzzo | 2 | 305 | 33.35 |
| Stavros Tripakis | 3 | 2181 | 138.07 |
| Alberto L. Sangiovanni-Vincentelli | 4 | 11385 | 1881.40 |