Name
Abstract | ||
|---|---|---|
It is our belief that the formal design of real-world concurrent systems does not fit well with model/state-oriented specification languages such as the Z notation. The problem with such systems is that they not only expose complex functional requirements but also critical control-level aspects such as concurrency. On the other hand, the most widely-spread formal languages dealing with concurrency, namely Petri-nets, reveal weaknesses (mostly state-space explosion) when dealing with complex functional requirements. In this paper, we propose a hybrid methodology, based on the traditional Z notation for the functional part of the system and using Petri-nets to model its concurrent control. We describe a simple method to derive new proof obligations in case of possible concurrent activation of Z operations, as modeled by the associated Petri-nets. By keeping the interface between both worlds as thin as possible, we do not put into question the interesting properties of the Z language: expressiveness, modularity and support for refinement. Moreover, our petri-based concurrent activation networks only address concurrency issues. Hence, it is likely that they remain manageable in term of state-space and so analyzable using existing Petri-net tools. We experimented this exploratory method on a real application, a research middleware kernel, which is now fully operational. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1007/3-540-44880-2_6 | ZB |
Keywords | Field | DocType |
z operation,concurrent control,z language,real-world concurrent system,z notation,possible concurrent activation,associated petri-nets,traditional z notation,petri-based concurrent activation network,complex functional requirement,concurrency control,specification language,middleware,state space,formal language,petri net,functional requirement,active network | Specification language,Z notation,Petri net,Programming language,Concurrency control,Concurrent engineering,Computer science,Concurrency,Formal specification,Artificial intelligence,Concurrent object-oriented programming,Distributed computing | Conference |
Volume | ISSN | ISBN |
2651 | 0302-9743 | 3-540-40253-5 |
Citations | PageRank | References |
1 | 0.37 | 7 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Frédéric Peschanski | 1 | 47 | 11.12 |
| David Julien | 2 | 5 | 1.20 |