Paper Info
Title
An operational semantics in UTP for a language of reactive designs (abstract)
Abstract
Following the approach in UTP, we describe a language of state-rich processes with communication, concurrency, and imperative commands on program variables. We give this language an operational semantics, with states and transitions represented symbolically. The semantics is described in Z, allowing us to execute the semantics using an animator, and to start work on a mechanical proof of correctness using the deep embedding in ProofPowerZ of the existing denotational semantics for the language. An extension of the operational semantics has been used in an algorithm to construct automata as part of the Circus model checker. This is joint work with Ana Cavalcanti and Leonardo Freitas.
Year
DOI
Venue
2006
10.1007/11768173_5
UTP
Keywords
Field
DocType
reactive design,joint work,program variable,leonardo freitas,operational semantics,existing denotational semantics,ana cavalcanti,imperative command,circus model checker,deep embedding,mechanical proof
Formal semantics (linguistics),Operational semantics,Programming language,Computational semantics,Computer science,Denotational semantics,Communicating sequential processes,Action semantics,Algorithm,Failure semantics,Theoretical computer science,Well-founded semantics
Conference
ISBN
Citations 
PageRank 
3-540-34750-X
0
0.34
References 
Authors
1
1
Name
Order
Citations
PageRank
Jim Woodcock124418.34