Submitted Paper
| ID | 9 |
| Submitted | 2006-04-14 |
| Last Update | |
| Title | Verification of Behavioural Refinement |
| Author(s) | Author #1 Name: Agnès Arnould Org: Université de Poitiers Country: France Email: agnes.arnould@univ-poitiers.fr Author #2 Name: Pascale Le Gall Org: Université d'Évry Val d'Essone Country: France Email: legall@lami.univ-evry.fr Author #3 Name: Till Mossakowski Org: University of Bremen Country: Germany Email: till@informatik.uni-bremen.de |
| Other Author(s) | |
| Contact Author | Author #1 Alt Email: arnould@sic.sp2mi.univ-poitiers.fr Telephone: (33) 5 49 49 68 64 |
| Keywords | behavioural semantics, refinement, proof, testing, CASL, institutions. |
| Abstract | CASL is a language for expressing formal developments of software.
Recently, a refinement language for CASL has been proposed. Now refinement steps typically involve behavioural interpretation of the refined specifications: the implementing specification or program need not to satisfy the initial requirements literally, but only its observable behaviour has to do so. Following recent work on behavioural semantics for CASL specifications, we recall a simple notion of behavioural refinement. The main contribution is then the development of suitable proof and test support for the verification of behavioural refinement. Regarding proof technics, we enrich the specification by specifying observable contexts and modeling the behavioural quotient. This encoding that transforms out the behavioural nature, ending up in an ordinary refinement. The latter can then be tackled with known tools for structured theorem proving. Regarding test technics, they are fitting to the behavioural framework since correctness is usually defined up to the set of observations which may be deduced from the executions performed on the program under test. The already well-established black-box testing methods are extended to the test of behavioural refinement. Finally, we also stetch how these two technics of proving and testing can be combined together to provide flexible verification strategies. |
| Topics | |
| Comments | |
| Paper | 9.pdf (41KB) |