@tasawer

Refinement in Circus

, , и . FME 2002:Formal Methods—Getting IT Right, том 2391 из Lecture Notes in Computer Science, Springer Berlin / Heidelberg, 10.1007/3-540-45614-7_26.(2002)

Аннотация

We describe refinement in Circus, a concurrent specification language that integrates imperative CSP, Z, and the refinement calculus. Each Circus process has a state and accompanying actions that define both the internal state transitions and the changes in control flow that occur during execution. We define the meaning of refinement of processes and their actions, and propose a sound data refinement technique for process refinement. Refinement laws for CSP and Z are directly relevant and applicable to Circus, but our focus here is on new laws for processes that integrate state and control. We give some new results about the distribution of data refinement through the combinators of CSP. We illustrate our ideas with the development of a distributed system of cooperating processes from a centralised specification.

Линки и ресурсы

тэги

    сообщество

    • @tasawer
    • @dblp
    • @leonardo
    @tasawer- тэги данного пользователя выделены