Sciweavers

Share
ENTCS
2008

ArcAngelC: a Refinement Tactic Language for Circus

9 years 2 months ago
ArcAngelC: a Refinement Tactic Language for Circus
Circus is a refinement language, in which specifications define both data and behavioural aspects of concurrent systems using a combination of Z and CSP. Its refinement theory and calculus are distinctive, but refinements may be long and repetitive, and using this technique can be hard. Some useful strategies have already been identified, described, and used. By documenting and using them as tactics, a lot can be gained since they can be repeatedly used as single transformation rules. Here, we present ArcAngelC, a language for defining such refinement tactics; we present the language and its application in the formalisation of an existing informal strategy for verification of Ada implementations of control systems. Key words: Concurrency, refinement calculus, tactics, control law diagrams.
M. V. M. Oliveira, A. L. C. Cavalcanti
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where ENTCS
Authors M. V. M. Oliveira, A. L. C. Cavalcanti
Comments (0)
books