Paper Info
Title
Implementing tactics of refinement in CRefine
Abstract
Circus is a formal language that combines Z and CSP, providing support for specification of both data and behavioural aspects of concurrent systems. Furthermore, Circus has an associated refinement calculus, which can be used to develop software in a precise and stepwise fashion. Each step is justified by the application of a refinement law (possibly with the discharge of proof obligations). Sometimes, the same laws can be applied in the same manner in different developments or even in different parts of a single development. A strategy to optimize this calculus is to formalise this application as a refinement tactic, which can then be used as a single transformation rule. CRefine was developed to automate the Circus refinement calculus. However, before the work presented here, it did not provide support for refinement tactics. In this paper, we present an extension to CRefine: a new module that automates the process of defining and applying refinement tactics formalised in the tactic language ArcAngel C. Finally, we illustrate the usefulness of the extension in the development of an industrial case study.
Year
DOI
Venue
2012
10.1007/978-3-642-33826-7_24
SEFM
Keywords
Field
DocType
tactic language arcangel c.,single development,refinement law,implementing tactic,different part,refinement tactic,single transformation rule,formal language,different development,circus refinement calculus,associated refinement calculus
Formal language,Programming language,Systems engineering,Refinement calculus,Computer science,Software,Refinement,Artificial intelligence
Conference
Citations 
PageRank 
References 
0
0.34
11
Authors
2
Name
Order
Citations
PageRank
Madiel Conserva Filho121.46
Marcel Vinicius Medeiros Oliveira2606.53