Specification refinements: Calculi, tools, and applications

Mihai Codescu, Till Mossakowski, Donald Sannella, Andrzej Tarlecki

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

We propose and study a framework for systematic development of software systems (or models) from their formal specifications. We introduce a language for formal development by refinement and decomposition, as an extension to CASL. We complement it with a notion of refinement tree and present proof calculi for checking correctness of refinements as well as their consistency. Both calculi have been implemented in the Heterogeneous Tool Set (Hets), and have been integrated with other tools like model finders and conservativity checkers.
Original languageEnglish
Pages (from-to)1-49
Number of pages49
JournalScience of Computer Programming
Volume144
Early online date26 Apr 2017
DOIs
Publication statusPublished - 15 Sept 2017

Fingerprint

Dive into the research topics of 'Specification refinements: Calculi, tools, and applications'. Together they form a unique fingerprint.

Cite this