Liveness properties in CafeOBJ
A case study for meta-level specifications
 |
- Norbert Preining
- Research Center for Software Verification
|
| Date: |
2014/08/07 (Thu) 15:00 to 17:00 |
| Place: |
JAIST Collaboration Room 6 (I57-g) |
| Group: |
Research Center for Software Verification |
We provide an innovative development of algebraic specifications and proof scores in CafeOBJ by extending a base specification to the meta-level that includs infinite transition sequences. The infinite transition sequences are modeled using behavioral specification with hidden sort, and make it possible to prove safety and liveness properties in an uniform way.
As an example of the development, we present a specification of Dijkstra's binary semaphore, a protocol to guarantee exclusive access to a resource. For this protocol we will give three different properties, one being the mutual exclusion (or safety) property, and two more regarding different forms of liveness, which we call progress property and entrance property. These three properties are verified in a computational (by term rewriting) way uniformly based on the new development.
Besides being a case study of modeling meta-properties in CafeOBJ, we provide an initial characterization of strength of various properties. Furthermore, this method can serve as a blue-print for other specifications, in particular those based on Abstract State Systems.
