Title: Refinement of eb 3 Process Patterns into B Specifications
Abstract: On one hand, eb 3 is a trace-based formal language created for the specification of information systems (IS). In particular, eb 3 points out the dynamic behaviour of the system. On the other hand, B is a state-based formal language well adapted for the specification of the IS static properties. We are defining a new approach called eb 4 that integrates both eb 3 and B to specify IS. eb 3 process expressions are used to represent and validate the behaviour of the system. Then, the specification is translated into B in order to specify and verify the main static properties of the IS. In this paper, we deal with the refinement of eb 3 process expressions into B specifications. Since this process cannot be automated, we define refinement patterns that can be reused to obtain B specifications that refine the event ordering properties specified in eb 3.
Publication Year: 2006
Publication Date: 2006-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 3
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot