Specification refinements: Calculi, tools, and applications

Mihai Codescu; Till Mossakowski; Donald Sannella; Andrzej Tarlecki

doi:10.1016/j.scico.2017.04.005

Specification refinements: Calculi, tools, and applications

Mihai Codescu, Till Mossakowski, Donald Sannella, Andrzej Tarlecki

Research output: Contribution to journal › Article › peer-review

Abstract

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 language	English
Pages (from-to)	1-49
Number of pages	49
Journal	Science of Computer Programming
Volume	144
Early online date	26 Apr 2017
DOIs	https://doi.org/10.1016/j.scico.2017.04.005
Publication status	Published - 15 Sep 2017

Access to Document

10.1016/j.scico.2017.04.005Licence: All Rights Reserved

casl-refinement-scp-1Accepted author manuscript, 485 KB

http://www.sciencedirect.com/science/article/pii/S0167642317300801Licence: All Rights Reserved

Don Sannella
- dtsinf.ed.acuk
- School of Informatics - PERSONAL CHAIR IN COMPUTER SCIENCE
- Laboratory for Foundations of Computer Science
- Foundations of Computation
Person: Academic: Research Active

Cite this

@article{2b728715747842b99d9e9d277a870dd1,

title = "Specification refinements: Calculi, tools, and applications",

abstract = "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.",

author = "Mihai Codescu and Till Mossakowski and Donald Sannella and Andrzej Tarlecki",

year = "2017",

month = sep,

day = "15",

doi = "10.1016/j.scico.2017.04.005",

language = "English",

volume = "144",

pages = "1--49",

journal = "Science of Computer Programming",

issn = "0167-6423",

publisher = "Elsevier",

}

TY - JOUR

T1 - Specification refinements: Calculi, tools, and applications

AU - Codescu, Mihai

AU - Mossakowski, Till

AU - Sannella, Donald

AU - Tarlecki, Andrzej

PY - 2017/9/15

Y1 - 2017/9/15

N2 - 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.

AB - 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.

U2 - 10.1016/j.scico.2017.04.005

DO - 10.1016/j.scico.2017.04.005

M3 - Article

VL - 144

SP - 1

EP - 49

JO - Science of Computer Programming

JF - Science of Computer Programming

SN - 0167-6423

ER -

Specification refinements: Calculi, tools, and applications

Abstract

Access to Document

Fingerprint

Profiles

Don Sannella

Cite this