id: 05904440
dt: j
an: 05904440
au: Oliveira, Marcel; Zeyda, Frank; Cavalcanti, Ana
ti: A tactic language for refinement of state-rich concurrent specifications.
so: Sci. Comput. Program. 76, No. 9, 792-833 (2011).
py: 2011
pu: Elsevier Science B.V. (North-Holland), Amsterdam
la: EN
cc: 
ut: concurrency; refinement calculus; tactics; control law diagrams
ci: 
li: doi:10.1016/j.scico.2010.11.012
ab: Summary: 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 since refinements may be long and repetitive, the
    practical application of this technique can be hard. Useful strategies
    have been identified, described, and used, and by documenting them as
    tactics, they can be expressed and repeatedly applied as single
    transformation rules. Here, we present ArcAngel$C$, a language for
    defining such tactics; we present the language, its semantics, and its
    application in the formalisation of an existing strategy for
    verification of Ada implementations of control systems specified by
    Simulink diagrams. We also discuss its mechanisation in a theorem
    prover, ProofPower-Z.
rv: