Name
Abstract | ||
|---|---|---|
The idea to use simulations (or refinements) as a compositional abstraction device is well-known, both in untimed and timed settings, and has already been studied theoretically and practically in many papers during the last three decades. Nevertheless, existing approaches do not handle two fundamental modeling concepts which, for instance, are frequently used in the popular Uppaalmodel checker: (1) a parallel composition operator that supports communication via shared variables as well as synchronization of actions, and (2) committed locations. We describe a framework for compositional abstraction based on simulation relations that does support both concepts, and that is suitable for Uppaal. Our approach is very general and the only essential restriction is that the guards of input transitions do not depend on external variables. We have applied our compositional framework to verify the Zeroconf protocol for an arbitrary number of hosts. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-85778-5_17 | Applied Categorical Structures |
Keywords | Field | DocType |
real-time model checking,committed location,compositional abstraction,compositional abstraction device,arbitrary number,zeroconf protocol,external variable,input transition,essential restriction,compositional framework,fundamental modeling concept,real time,model checking | Abstraction model checking,Synchronization,Fundamental modeling concepts,Model checking,Abstraction,Zero-configuration networking,Programming language,Computer science,External variable,Theoretical computer science,Composition operator | Conference |
Volume | ISSN | Citations |
5215 | 0302-9743 | 10 |
PageRank | References | Authors |
0.68 | 20 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jasper Berendsen | 1 | 50 | 5.22 |
| Frits Vaandrager | 2 | 1571 | 105.12 |