We propose and study a framework for systematic
development of software systems (or models) from their
formal specification.
We introduce a language for refinement and branching of formal
developments. 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.
%0 Journal Article
%1 codescu2017specification
%A Codescu, Mihai
%A Mossakowski, Till
%A Sannella, Donald
%A Tarlecki, Andrzej
%D 2017
%J Science of Computer Programming
%K casl imported institution logic myown
%P 1–49
%R 10.1016/j.scico.2017.04.005
%T Specification refinements: calculi, tools, and applications
%U https://www.sciencedirect.com/science/article/pii/S0167642317300801
%V 144
%X We propose and study a framework for systematic
development of software systems (or models) from their
formal specification.
We introduce a language for refinement and branching of formal
developments. 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.
@article{codescu2017specification,
abstract = { We propose and study a framework for systematic
development of software systems (or models) from their
formal specification.
We introduce a language for refinement and branching of formal
developments. 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. },
added-at = {2016-11-19T18:07:25.000+0100},
author = {Codescu, Mihai and Mossakowski, Till and Sannella, Donald and Tarlecki, Andrzej},
biburl = {https://www.bibsonomy.org/bibtex/2324d978258ac74c4720c76b68ee28cda/tillmo},
doi = {10.1016/j.scico.2017.04.005},
interhash = {70b666e1d31aa3feaadb340c48f201ce},
intrahash = {324d978258ac74c4720c76b68ee28cda},
journal = { Science of Computer Programming},
keywords = {casl imported institution logic myown},
pages = {1–49},
timestamp = {2017-11-09T12:29:09.000+0100},
title = {Specification refinements: calculi, tools, and applications},
url = {https://www.sciencedirect.com/science/article/pii/S0167642317300801},
volume = 144,
year = 2017
}