Name
Abstract | ||
|---|---|---|
Two styles of description arise naturally in formal specification: state-based and behavioural. In state-based notations, a system is characterised by a collection of variables, and their values determine which actions may occur throughout a system history. Behavioural specifications describe the chronologies of actions—interactions between a system and its environment. The exact nature of such interactions is captured in a variety of semantic models with corresponding notions of refinement; refinement in state based systems is based on the semantics of sequential programs and is modelled relationally. Acknowledging that these viewpoints are complementary, substantial research has gone into combining the paradigms. The purpose of this paper is to do three things. First, we survey recent results linking the relational model of refinement to the process algebraic models. Specifically, we detail how variations in the relational framework lead to relational data refinement being in correspondence with traces–divergences, singleton failures and failures–divergences refinement in a process semantics. Second, we generalise these results by providing a general flexible scheme for incorporating the two main “erroneous” concurrent behaviours: deadlock and divergence, into relational refinement. This is shown to subsume previous characterisations. In doing this we derive relational refinement rules for specifications containing both internal operations and outputs that corresponds to failures–divergences refinement. Third, the theory has been formally specified and verified using the interactive theorem prover KIV. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/s00165-007-0066-z | Formal Asp. Comput. |
Keywords | Field | DocType |
model specification,deadlock,relational model,formal specification,computer programming,semantic model,relational data,theorem prover,process algebra | Relational calculus,Programming language,Refinement calculus,Relational database,Computer science,Deadlock,Formal specification,Theoretical computer science,Refinement,Relational model,Proof assistant | Journal |
Volume | Issue | ISSN |
21 | 1-2 | 1433-299X |
Citations | PageRank | References |
13 | 0.59 | 27 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Eerke A. Boiten | 1 | 423 | 37.81 |
| John Derrick | 2 | 359 | 24.96 |
| Gerhard Schellhorn | 3 | 769 | 56.43 |