28
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Unifying Theories of Reactive Design Contracts

      Preprint
      , , , ,

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          Design-by-contract is an important technique for model-based design in which a composite system is specified by a collection of contracts that specify the behavioural assumptions and guarantees of each component. In this paper, we describe a unifying theory for reactive design contracts that provides the basis for modelling and verification of reactive systems. We provide a language for expression and composition of contracts that is supported by a rich calculational theory. In contrast with other semantic models in the literature, our theory of contracts allow us to specify both the evolution of state variables and the permissible interactions with the environment. Moreover, our model of interaction is abstract, and supports, for instance, discrete time, continuous time, and hybrid computational models. Being based in Unifying Theories of Programming (UTP), our theory can be composed with further computational theories to support semantics for multi-paradigm languages. Practical reasoning support is provided via our proof framework, Isabelle/UTP, including a proof tactic that reduces a conjecture about a reactive program to three predicates, characterising its assumptions and guarantees about intermediate and final observations. Our work advances the state-of-the-art in semantics for reactive languages, description of their contractual specifications, and compositional verification.

          Related collections

          Most cited references38

          • Record: found
          • Abstract: not found
          • Article: not found

          An axiomatic basis for computer programming

          C. Hoare (1969)
            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            A lattice-theoretical fixpoint theorem and its applications

              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              A Theory of Communicating Sequential Processes

                Bookmark

                Author and article information

                Journal
                29 December 2017
                Article
                1712.10233
                57c7f0b3-f24b-4754-bfad-83f4933c3276

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                53 pages, submitted to Journal of Theoretical Computer Science December 2017
                cs.LO

                Comments

                Comment on this article