| Download | - View accepted manuscript: Architecture-Driven Verification of Concurrent Systems (PDF, 797 KiB)
|
|---|
| Author | Search for: Erdogmus, Hakan |
|---|
| Format | Text, Article |
|---|
| Subject | architecture-based verification; architectural specifications; architectural formalisms; model checking; equivalence checking; compositional verification.; spécification architecturale; formalisme architectural; vérification de modèle; vérification de l'équivalence; vérification compositionnelle |
|---|
| Abstract | This paper proposes a method to construct a set of proof obligations from the architectural specification of a concurrent system. The architectural specifications used express correctness requirements of a concurrent system at a high level without any reference to component functionality. Then the proof obligations derived from such specifications are discharged as model checking tasks in a suitable behavioral model where components are assigned their respective functionalities. An experimental extension to the SPIN tool is used as the model checker. The block diagram notation used to specify architectures allows interchangeable components with equivalent intended functionalities to be encapsulated within a representative module. A proof obligation of such a system is discharged as an equivalence checking task in the behavioral model chosen. It is shown how infeasible proof obligations can be decomposed by decomposing the architectural specification. Obligation decomposition relies on assume-guarantee conditions. |
|---|
| Publication date | 1997 |
|---|
| In | |
|---|
| Language | English |
|---|
| NRC number | NRCC 41549 |
|---|
| NPARC number | 5764623 |
|---|
| Export citation | Export as RIS |
|---|
| Report a correction | Report a correction (opens in a new tab) |
|---|
| Record identifier | abb9b207-f404-42d0-8d05-2d95adbf15e9 |
|---|
| Record created | 2009-03-29 |
|---|
| Record modified | 2020-03-20 |
|---|
