We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
A trace-based service semantics guaranteeing deadlock freedom.
- Authors
Stahl, Christian; Vogler, Walter
- Abstract
We revise the accordance preorder in the context of deadlock freedom for asynchronously communicating services. Accordance considers all controllers of a service-that is, all environments that can interact with the service without deadlocking. A service Impl accords with a service Spec if every controller of Spec is also a controller of Impl. We model finite-state and infinite-state services as Petri nets and formalize the semantics of such models with a traditional concurrency semantics, a trace-based semantics. As benefits, we get an easier characterization of the accordance preorder, prove that it is a fully abstract precongruence, and present an algorithm to decide refinement of two finite-state services. Previously, operating guidelines have been introduced to study the behavior of finite-state services; they characterize all controllers of a given service and can be used to decide accordance. An operating guideline is a finite automaton annotated with Boolean formulae that describes the semantics of a service from the perspective of its controllers rather than from the perspective of the service. We show that our trace-based semantics can be translated back and forth into operating guidelines, thereby providing a more conceptual understanding of operating guidelines.
- Subjects
SEMANTIC computing; ELECTRONIC controllers; PROGRAMMING language semantics; ASYNCHRONOUS circuits; PROGRAMMABLE controllers; MATHEMATICAL analysis
- Publication
Acta Informatica, 2012, Vol 49, Issue 2, p69
- ISSN
0001-5903
- Publication type
Article
- DOI
10.1007/s00236-012-0151-5