Department of Computer Science

Publications

Papers

  • 1. A. Miyazawa, P. Ribeiro, L. Wei, A. L. C. Cavalcanti, J. Timmis, J. C. P. Woodcock: RoboChart: modelling and verification of the functional behaviour of robotic applications. Software & Systems Modeling. (2019).

    Robots are becoming ubiquitous: from vacuum cleaners to driverless cars, there is a wide variety of applications, many with potential safety hazards. The work presented in this paper proposes a set of constructs suitable for both modelling robotic applications and supporting verification via model checking and theorem proving. Our goal is to support roboticists in writing models and applying modern verification techniques using a language familiar to them. To that end, we present RoboChart, a domain-specific modelling language based on UML, but with a restricted set of constructs to enable a simplified semantics and automated reasoning. We present the RoboChart metamodel, its well-formedness rules, and its process-algebraic semantics. We discuss verification based on these foundations using an implementation of RoboChart and its semantics as a set of Eclipse plug-ins called RoboTool.

    @article{Miyazawa2019,
      author = {A.~Miyazawa and P.~Ribeiro and L.~Wei and A.~L.~C.~Cavalcanti and J.~Timmis and J.~C.~P.~Woodcock},
      title = {RoboChart: modelling and verification of the functional behaviour of robotic applications},
      journal = {Software {\&} Systems Modeling},
      year = {2019},
      month = jan,
      day = {23},
      issn = {1619-1374},
      doi = {10.1007/s10270-018-00710-z},
      url = {https://doi.org/10.1007/s10270-018-00710-z}
    }
    
  • 2. P. Ribeiro, A. L. C. Cavalcanti: Angelic processes for CSP via the UTP. Theoretical Computer Science. 756, 19–63 (2019).

    Demonic and angelic nondeterminism play fundamental roles as abstraction mechanisms for formal modelling. In contrast with its demonic counterpart, in an angelic choice failure is avoided whenever possible. Although it has been extensively studied in refinement calculi, in the context of process algebras, and of the Communicating Sequential Processes (CSP) algebra for refinement, in particular, it has been elusive. We show here that a semantics for an extended version of CSP that includes both demonic and angelic choice can be provided using Hoare and He’s Unifying Theories of Programming (UTP). Since CSP is given semantics in the UTP via reactive designs (pre and postcondition pairs) we have developed a theory of angelic designs and a conservative extension of the CSP theory using reactive angelic designs. To characterise angelic nondeterminism appropriately in an algebra of processes, however, a notion of divergence that can undo the history of events needs to be considered. Taking this view, we present a model for CSP where angelic choice completely avoids divergence just like in the refinement calculi for sequential programs.

    @article{Ribeiro2019a,
      groups = {papers},
      keywords = { Semantics, Formal specification, Process algebras, CSP, UTP },
      author = {P.~Ribeiro and A.~L.~C.~Cavalcanti},
      url = {https://www-users.cs.york.ac.uk/%7Epfr/publications/TCS2018.pdf},
      doi = {10.1016/j.tcs.2018.10.008},
      issn = {0304-3975},
      year = {2019},
      pages = {19-63},
      volume = {756},
      journal = {Theoretical Computer Science},
      title = {Angelic processes for CSP via the UTP}
    }
    
  • 3. A. Miyazawa, A. L. C. Cavalcanti, A. Wellings: SCJ-Circus: specification and refinement of Safety-Critical Java programs. Science of Computer Programming. (2019).

    Safety-Critical Java (SCJ) is a version of Java for real-time, embedded, safety-critical applications. It supports certification via abstractions that enforce a particular program architecture, with controlled concurrency and memory models. SCJ is an Open Group standard, with a reference implementation, but little support for reasoning. Here, we present SCJ-Circus, a refinement notation for specification and verification of low-level models of SCJ programs. SCJ-Circus is part of the Circus family of state-rich process algebras: it includes the Circus constructs for modelling of sequential and concurrent behaviour based on Z and CSP, and the real-time and object-oriented extensions of Circus, in addition to the SCJ abstractions. We present the syntax of SCJ-Circus and its semantics, defined by mapping SCJ-Circus constructs to those of Circus. We also detail a refinement strategy that takes a Circus design that adheres to a multiprocessor cyclic executive pattern and produces an SCJ program design, described in SCJ-Circus. Finally, we show how this refinement strategy can be extended for more complex program architectures.

    @article{Miyazawa2019a,
      groups = { hijac, papers },
      keywords = { SCJ, missions, event handlers, process algebra, semantics, refinement },
      author = {A.~Miyazawa and A.~L.~C.~Cavalcanti and A.~Wellings},
      url = {http://www.sciencedirect.com/science/article/pii/S0167642319300012},
      doi = {10.1016/j.scico.2019.01.002},
      issn = {0167-6423},
      year = {2019},
      journal = {Science of Computer Programming},
      title = {SCJ-Circus: specification and refinement of Safety-Critical Java programs}
    }
    
  • 4. A. L. C. Cavalcanti, A. C. A. Sampaio, A. Miyazawa, P. Ribeiro, M. S. Conserva Filho, A. Didier, W. Li, J. Timmis: Verified simulation for robotics. Science of Computer Programming. 174, 1–37 (2019).

    Simulation is a favoured technique for analysis of robotic systems. Currently, however, simulations are programmed in an ad hoc way, for specific simulators, using either proprietary languages or general languages like C or C++. Even when a higher-level language is used, no clear relation between the simulation and a design model is established. We describe a tool-independent notation called RoboSim, designed specifically for modelling of (verified) simulations. We describe the syntax, well-formedness conditions, and semantics of RoboSim. We also show how we can use RoboSim models to check if a simulation is consistent with a functional design written in a UML-like notation akin to those often used by practitioners on an informal basis. We show how to check whether the design enables a feasible scheduling of behaviours in cycles as needed for a simulation, and formalise implicit assumptions routinely made when programming simulations. We develop a running example and three additional case studies to illustrate RoboSim and the proposed verification techniques. Tool support is also briefly discussed. Our results enable the description of simulations using tool-independent diagrammatic models amenable to verification and automatic generation of code.

    @article{Cavalcanti2019a,
      groups = { robocalc, papers },
      keywords = { State machines, Process algebra, CSP, Semantics, Refinement },
      author = {A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio and A.~Miyazawa and P.~Ribeiro and M.~S.~Conserva~Filho and A.~Didier and W.~Li and J.~Timmis},
      url = {https://www-users.cs.york.ac.uk/%7Ealcc/publications/papers/CSMRCD19.pdf},
      doi = {10.1016/j.scico.2019.01.004},
      issn = {0167-6423},
      year = {2019},
      pages = {1-37},
      volume = {174},
      journal = {Science of Computer Programming},
      title = {Verified simulation for robotics}
    }
    
  • 5. S. Foster, A. L. C. Cavalcanti, J. C. P. Woodcock, F. Zeyda: Unifying theories of time with generalised reactive processes . Information Processing Letters. 135, 47–52 (2018).

    Hoare and He’s theory of reactive processes provides a unifying foundation for the formal semantics of concurrent and reactive languages. Though highly applicable, their theory is limited to models that can express event histories as discrete sequences. In this paper, we show how their theory can be generalised by using an abstract trace algebra. We show how the algebra, notably, allows us to consider continuous-time traces and thereby facilitate models of hybrid systems. We then use this algebra to reconstruct the theory of reactive processes in our generic setting, and prove characteristic laws for sequential and parallel processes, all of which have been mechanically verified in the Isabelle/HOL proof assistant.

    @article{FCWZ18,
      title = {Unifying theories of time with generalised reactive processes },
      journal = {Information Processing Letters},
      volume = {135},
      pages = {47 - 52},
      month = jul,
      year = {2018},
      doi = {10.1016/j.ipl.2018.02.017},
      author = {S.~Foster and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock and F.~Zeyda}
    }
    
  • 6. M. S. Conserva Filho, M. V. M. Oliveira, A. C. A. Sampaio, A. L. C. Cavalcanti: Compositional and Local Livelock Analysis for CSP. Information Processing Letters. 133, 21–25 (2018).

    The success of component-based techniques for software construction relies on trust in the emergent behaviour of the compositions. Here, we propose an efficient correct-by-construction technique for building livelock-free CSP models. Its verification conditions are based on a local analysis of the shortest event sequences (traces) that represent a recursive behaviour in the CSP model. This affords significant gains in performance in model checking. We evaluate our strategy based on models of the Milner’s scheduler and the dining philosophers.

    @article{COSC18,
      title = {Compositional and Local Livelock Analysis for {CSP}},
      pages = {21 - 25},
      journal = {Information Processing Letters},
      volume = {133},
      issn = {0020-0190},
      month = may,
      year = {2018},
      doi = {10.1016/j.ipl.2017.12.011},
      author = {M.~S.~Conserva~Filho and M.~V.~M.~Oliveira and A.~C.~A.~Sampaio and A.~L.~C.~Cavalcanti}
    }
    
  • 7. S. Foster, J. Baxter, A. L. C. Cavalcanti, A. Miyazawa, J. C. P. Woodcock: Automating Verification of State Machines with Reactive Designs and Isabelle/UTP. In: Formal Aspects of Component Software. pp. 137–155. Springer International Publishing, Cham (2018).
    @inproceedings{Foster2018a,
      groups = { robocalc, isabelle-utp, papers },
      publisher = {Springer International Publishing},
      address = { Cham },
      pages = {137--155},
      year = {2018},
      booktitle = {Formal Aspects of Component Software},
      title = {Automating Verification of State Machines with Reactive Designs and Isabelle/UTP},
      url = {https://pure.york.ac.uk/portal/services/downloadRegister/55606873/1807.08588.pdf},
      doi = {10.1007/978-3-030-02146-7_7},
      author = {S.~Foster and J.~Baxter and A.~L.~C.~Cavalcanti and A.~Miyazawa and J.~C.~P.~Woodcock}
    }
    
  • 8. A. L. C. Cavalcanti, A. Miyazawa, A. C. A. Sampaio, W. Li, P. Ribeiro, J. Timmis: Modelling and Verification for Swarm Robotics. In: Integrated Formal Methods. pp. 1–19. Springer International Publishing, Cham (2018).

    RoboChart is a graphical domain-specific language, based on UML, but tailored for the modelling and verification of single robot systems. In this paper, we introduce RoboChart facilities for modelling and verifying heterogeneous collections of interacting robots. We propose a new construct that describes the collection itself, and a new communication construct that allows fine-grained control over the communication patterns of the robots. Using these novel constructs, we apply RoboChart to model a simple yet powerful and widely used algorithm to maintain the aggregation of a swarm. Our constructs can be useful also in the context of other diagrammatic languages, including UML, to describe collections of arbitrary interacting entities.

    @inproceedings{Cavalcanti2018a,
      groups = { robocalc, papers },
      isbn = { 978-3-319-98938-9 },
      pages = {1--19},
      address = {Cham},
      publisher = {Springer International Publishing},
      year = {2018},
      booktitle = {Integrated Formal Methods},
      title = {Modelling and Verification for Swarm Robotics},
      author = {A.~L.~C.~Cavalcanti and A.~Miyazawa and A.~C.~A.~Sampaio and W.~Li and P.~Ribeiro and J.~Timmis}
    }
    
  • 9. S. Foster, K. Ye, A. L. C. Cavalcanti, J. C. P. Woodcock: Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. In: Relational and Algebraic Methods in Computer Science. pp. 205–224. Springer International Publishing, Cham (2018).

    Reactive programs are ubiquitous in modern applications, and so verification is highly desirable. We present a verification strategy for reactive programs with a large or infinite state space utilising algebraic laws for reactive relations. We define novel operators to characterise interactions and state updates, and an associated equational theory. With this we can calculate a reactive program’s denotational semantics, and thereby facilitate automated proof. Of note is our reasoning support for iterative programs with reactive invariants, which is supported by Kleene algebra. We illustrate our strategy by verifying a reactive buffer. Our laws and strategy are mechanised in Isabelle/UTP, which provides soundness guarantees, and practical verification support.

    @inproceedings{Foster2018b,
      groups = { papers },
      isbn = { 978-3-030-02149-8 },
      pages = {205--224},
      address = {Cham},
      publisher = {Springer International Publishing},
      year = {2018},
      booktitle = {Relational and Algebraic Methods in Computer Science},
      title = {Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra},
      url = {https://pure.york.ac.uk/portal/services/downloadRegister/55512660/RAMICS2018.pdf},
      doi = {10.1007/978-3-030-02149-8},
      author = {S.~Foster and K.~Ye and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock}
    }
    
  • 10. F. Zeyda, J. Ouy, S. Foster, A. L. C. Cavalcanti: Formalising Cosimulation Models. In: A. Cerone and M. Roveri (eds.) Software Engineering and Formal Methods - SEFM 2017 Collocated Workshops. pp. 453–468. Springer (2018).

    Cosimulation techniques are popular in the design and early testing of cyber-physical systems. Such systems are typically composed of heterogeneous components and specified using a variety of languages and tools; this makes their formal analysis beyond simulation challenging. We here present work on formalised models and proofs about cosimulations in our theorem prover Isabelle/UTP, illustrated by an industrial case study from the railways sector. Novel contributions are a mechanised encoding of the FMI framework for cosimulation, simplification and translation of (case-study) models into languages supported by our proof system, and an encoding of an FMI instantiation.

    @inproceedings{ZOFC18,
      author = {F.~Zeyda and J.~Ouy and S.~Foster and A.~L.~C.~Cavalcanti},
      title = {Formalising Cosimulation Models},
      booktitle = {Software Engineering and Formal Methods - {SEFM} 2017 Collocated Workshops},
      pages = {453--468},
      doi = {10.1007/978-3-319-74781-1_31},
      editor = {A.~Cerone and M.~Roveri},
      series = {Lecture Notes in Computer Science},
      volume = {10729},
      publisher = {Springer},
      year = {2018},
      url = {https://www-users.cs.york.ac.uk/%7Ealcc/publications/papers/ZOFC18.pdf}
    }
    
  • 11. W. Li, A. Miyazawa, P. Ribeiro, A. L. C. Cavalcanti, J. C. P. Woodcock, J. Timmis: From formalised state machines to implementation of robotic controllers. In: Groß, R. et al. (eds.) Distributed Autonomous Robotic Systems: The 13th International Symposium. pp. 517–529. Springer International Publishing (2018).

    High-level controllers for autonomous robotic systems can be specified using state machines. However, these are typically developed in an ad hoc manner without formal semantics, which makes it difficult to analyse the controller. Simulations are often used during the development, but a rigorous connection between the designed controller and the implementation is often overlooked. This paper presents a state-machine based notation, RoboChart, together with tools to automatically create code from the state machines, establishing a rigorous connection between specification and implementation. In RoboChart, the robot’s controller is specified either graphically or using a textual description language. The controller code for simulation is automatically generated through a direct mapping from the specification. We demonstrate our approach using two case studies (self-organized aggregation and swarm taxis) in swarm robotics. The simulations are presented using two different simulators showing the general applicability of our approach in a wide range of robotic controllers.

    @inbook{Li-etal2016,
      title = {From formalised state machines to implementation of robotic controllers},
      author = {W.~Li and A.~Miyazawa and P.~Ribeiro and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock and J.~Timmis},
      booktitle = {Distributed Autonomous Robotic Systems: The 13th International Symposium},
      year = {2018},
      pages = {517--529},
      doi = {10.1007/978-3-319-73008-0_36},
      isbn = {978-3-319-73008-0},
      series = {Springer Tracts in Advanced Robotics},
      publisher = {Springer International Publishing},
      editor = {Gro{\ss}, Roderich and Kolling, Andreas and Berman, Spring and Frazzoli, Emilio and Martinoli, Alcherio and Matsuno, Fumitoshi and Gauci, Melvin"},
      url = {https://arxiv.org/abs/1702.01783}
    }
    
  • 12. A. L. C. Cavalcanti, A. Miyazawa, R. Payne, J. Woodcock: Sound Simulation and Co-simulation for Robotics. In: M. Mazzara and B. Meyer (eds.) Present and Ulterior Software Engineering. pp. 173–194. Springer International Publishing (2017).

    Software engineering for modern robot applications needs attention; current practice suffers from costly iterations of trial and error, with hardware and environment in the loop. We propose the adoption of an approach to simulation and co-simulation of robotics applications where designs and (co-)simulations are amenable to verification. In this approach, designs are composed of several (co-)models whose relationship is defined using a SysML profile. Simulation is the favoured technique for analysis in industry, and co-simulation enables the orchestrated use of a variety of simulation tools, including, for instance, reactive simulators and simulators of control laws. Here, we define the SysML profile that we propose and give it a process algebraic semantics. With that semantics, we capture the properties of the SysML model that must be satisfied by a co-simulation. Our long-term goal is to support validation and verification beyond what can be achieved with simulation.

    @incollection{CMPW17,
      author = {A.~L.~C.~Cavalcanti and A.~Miyazawa and R.~Payne and J.~Woodcock},
      editor = {M.~Mazzara and B.~Meyer},
      title = {Sound Simulation and Co-simulation for Robotics},
      booktitle = {Present and Ulterior Software Engineering},
      year = {2017},
      publisher = {Springer International Publishing},
      pages = {173--194},
      doi = {10.1007/978-3-319-67425-4_11},
      url = {https://www-users.cs.york.ac.uk/%7Ealcc/publications/papers/CMPW17.pdf}
    }
    
  • 13. R. Otoni, A. L. C. Cavalcanti, A. C. A. Sampaio: Local Analysis of Determinism for CSP. In: S. Cavalheiro and J. Fiadeiro (eds.) Formal Methods: Foundations and Applications. pp. 107–124. Springer International Publishing (2017).

    Nondeterminism is an inevitable constituent of any theory that describes concurrency. For the validation and verification of concurrent systems, it is essential to investigate the presence or absence of nondeterminism, just as much as deadlock or livelock. CSP is a well established process algebra; the main tool for practical use of CSP, the model checker FDR, checks determinism using a global analysis. We propose a local analysis, in order to improve performance and scalability. Our strategy is to use a compositional approach where we start from basic deterministic processes and check whether any of the composition operators introduce nondeterminism. We present the algorithms used in our strategy and experiments that show the efficiency of our approach.

    @inproceedings{OCS17,
      author = {R.~Otoni and A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio},
      editor = {S.~Cavalheiro and J.~Fiadeiro},
      title = {Local Analysis of Determinism for CSP},
      booktitle = {Formal Methods: Foundations and Applications},
      year = {2017},
      publisher = {Springer International Publishing},
      pages = {107--124},
      volume = {10623},
      series = {Lecture Notes in Computer Science},
      doi = {10.1007/978-3-319-70848-5_8},
      url = {https://www-users.cs.york.ac.uk/%7Ealcc/publications/papers/OCS17.pdf}
    }
    
  • 14. A. Miyazawa, P. Ribeiro, W. Li, A. L. C. Cavalcanti, J. Timmis: Automatic Property Checking of Robotic Applications. In: The International Conference on Intelligent Robots and Systems. pp. 3869–3876 (2017).

    Robot software controllers are often concurrent and time critical, and requires modern engineering approaches for validation and verification. With this motivation, we have developed a tool and techniques for graphical modelling with support for automatic generation of underlying mathematical definitions for model checking. It is possible to check automatically both general properties, like absence of deadlock, and specific application properties. We cater both for timed and untimed modelling and verification. Our approach has been tried in examples used in a variety of robotic applications.

    @inproceedings{MRLCT17,
      author = {A.~Miyazawa and P.~Ribeiro and W.~Li and A.~L.~C.~Cavalcanti and J.~Timmis},
      title = {Automatic Property Checking of Robotic Applications},
      year = {2017},
      booktitle = {The International Conference on Intelligent Robots and Systems},
      pages = {3869-3876},
      doi = {10.1109/IROS.2017.8206238}
    }
    
  • 15. P. Ribeiro, A. Miyazawa, W. Li, A. L. C. Cavalcanti, J. Timmis: Modelling and Verification of Timed Robotic Controllers. In: N. Polikarpova and S. Schneider (eds.) Integrated Formal Methods. pp. 18–33. Springer (2017).

    Designing robotic systems can be very challenging, yet controllers are often specified using informal notations with development driven primarily by simulations and physical experiments, without relation to abstract models of requirements. The ability to perform formal analysis and replicate results across different robotic platforms is hindered by the lack of well-defined formal notations. In this paper we present a timed state-machine based formal notation for robotics that is informed by current practice. We motivate our work with an example from swarm robotics and define a compositional CSP-based discrete timed semantics suitable for refinement. Our results support verification and, importantly, enable rigorous connection with sound simulations and deployments.

    @inproceedings{Ribeiro2017,
      author = {P.~Ribeiro and A.~Miyazawa and W.~Li and A.~L.~C.~Cavalcanti and J.~Timmis},
      editor = {N.~Polikarpova and S.~Schneider},
      title = {Modelling and Verification of Timed Robotic Controllers},
      booktitle = {Integrated Formal Methods},
      year = {2017},
      publisher = {Springer},
      pages = {18--33},
      doi = {10.1007/978-3-319-66845-1_2},
      url = {https://www-users.cs.york.ac.uk/%7Ealcc/publications/papers/RMLCT17.pdf},
      isbn = {978-3-319-66845-1}
    }
    
  • 16. A. L. C. Cavalcanti, J. C. P. Woodcock, N. Amálio: Behavioural Models for FMI Co-simulations. In: A. C. A. Sampaio and F. Wang (eds.) International Colloquium on Theoretical Aspects of Computing. Springer (2016).

    Simulation is a favoured technique for analysis of cyberphysical systems. With their increase in complexity, co-simulation, which involves the coordinated use of heterogeneous models and tools, has become widespread. An industry standard, FMI, has been developed to support orchestration; we provide the first behavioural semantics of FMI. We use the state-rich process algebra, Circus, to present our modelling approach, and indicate how models can be automatically generated from a description of the individual simulations and their dependencies. We illustrate the work using three algorithms for orchestration. A stateless version of the models can be verified using model checking via translation to CSP. With that, we can prove important properties of these algorithms, like termination and determinism, for example. We also show that the example provided in the FMI standard is not a valid algorithm.

    @inproceedings{CWA16,
      booktitle = {International Colloquium on Theoretical Aspects of Computing},
      title = {{Behavioural Models for FMI Co-simulations}},
      editor = {A.~C.~A.~Sampaio and F.~Wang},
      author = {A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock and N.~Am\'alio},
      year = {2016},
      series = {Lecture Notes in Computer Science},
      publisher = {Springer},
      doi = {10.1007/978-3-319-46750-4_15},
      url = {https://www-users.cs.york.ac.uk/%7Ealcc/publications/papers/CWA16.pdf}
    }
    
  • 17. S. Foster, B. Thiele, A. L. C. Cavalcanti, J. C. P. Woodcock: Towards a UTP semantics for Modelica. In: Unifying Theories of Programming. Springer (2016).

    We describe our work on a UTP semantics for the dynamic systems modelling language Modelica. This is a language for modelling a system’s continuous behaviour using a combination of differential-algebraic equations and an event-handling system. We develop a novel UTP theory of hybrid relations, inspired by Hybrid CSP and Duration Calculus, that is purely relational and provides uniform handling of continuous and discrete variables. This theory is mechanised in our Isabelle implementation of the UTP, Isabelle/UTP, with which we verify some algebraic properties. Finally, we show how a subset of Modelica models can be given semantics using our theory. When combined with the wealth of existing UTP theories for discrete system modelling, our work enables a sound approach to heterogeneous semantics for Cyber-Physical systems by leveraging the theory linking facilities of the UTP.

    @inproceedings{FTCW16,
      booktitle = {Unifying Theories of Programming},
      title = {{Towards a UTP semantics for Modelica}},
      author = {S.~Foster and B.~Thiele and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
      year = {2016},
      series = {Lecture Notes in Computer Science},
      publisher = {Springer},
      doi = {10.1007/978-3-319-52228-9_3},
      url = {http://eprints.whiterose.ac.uk/105107/1/utp2016.pdf}
    }
    
  • 18. P. Ribeiro, A. L. C. Cavalcanti, J. C. P. Woodcock: A Stepwise Approach to Linking Theories. In: Unifying Theories of Programming. Springer International Publishing (2016).

    Formal modelling of complex systems requires catering for a variety of aspects. The Unifying Theories of Programming (UTP) distinguishes itself as a semantic framework that promotes unification of results across different modelling paradigms via linking functions. The naive composition of theories, however, may yield unexpected or undesirable semantic models. Here, we propose a stepwise approach to linking theories where we deal separately with the definition of the relation between the variables in the different theories and the identification of healthiness conditions. We explore this approach by deriving healthiness conditions for Circus Time via calculation, based on the healthiness conditions of CSP and a small set of principles underlying the timed model.

    @incollection{Ribeiro2016,
      title = {{A} {S}tepwise {A}pproach to {L}inking {T}heories},
      author = {P.~Ribeiro and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
      booktitle = {{U}nifying {T}heories of {P}rogramming},
      publisher = {Springer International Publishing},
      year = {2016},
      doi = {10.1007/978-3-319-52228-9_7},
      series = {{L}ecture {N}otes in {C}omputer {S}cience},
      url = {https://www-users.cs.york.ac.uk/%7Ealcc/publications/papers/RCW17.pdf}
    }
    

Technical Reports

  • 1. A. Cavalcanti, P. Ribeiro, A. Miyazawa, A. Sampaio, M. Conserva Filho, A. Didier: RoboSim Reference Manual. University of York (2019).

    In this report, we describe a UML-like notation calledRoboSim, designedspecifically for simulation of autonomous and mobile robots, and includingtimed primitives. We provide a reference manual forRoboSim. We describethe syntax, the well-formedness conditions and semantics ofRoboSim. Wealso present three case studies and show how we can useRoboSimmodelsto check if a simulation is consistent with a functional design written in aUML-like notation.

    @techreport{RoboSim,
      title = {{R}obo{S}im {R}eference {M}anual},
      author = {A.~Cavalcanti and P.~Ribeiro and A.~Miyazawa and A.~Sampaio and M.~Conserva~Filho and A.~Didier},
      institution = {University of York},
      year = {2019},
      month = mar,
      type = {{T}echnical report},
      url = {https://www.cs.york.ac.uk/circus/RoboCalc/robosim/robosim-reference.pdf}
    }
    
  • 2. A. Miyazawa, A. Cavalcanti, P. Ribeiro, W. Li, J. Woodcock, J. Timmis: RoboChart Reference Manual. University of York (2016).

    Autonomous and mobile robots are becoming ubiquitous. From domestic robotic vacuum cleaners to driverless cars, such robots interact with their environment and humans, leading to potential safety hazards. We propose a three-pronged solution to the problem of safety of mobile and autonomous robots: (1) domain-specific modelling with a formal underpinning; (2) automatic generation of sound simulations; and (3) verification based on model checking and theorem proving. Here, we report on a UML-like notation called RoboChart, designed specifically for modelling autonomous and mobile robots, and including timed and probabilistic primitives. We discuss a denotational semantics for a core subset of RoboChart, an approach for the development of sound simulations, and an implementation of RoboChart and its formal semantics as an Eclipse plugin supported by the CSP model checker FDR. This report is a reference manual for the RoboChart notation. It describes the syntax of RoboChart and its extensions, as well as the well-formedness conditions and semantics of the language constructs. Additionally, usage of the language is discussed via a application programming interface (API), simulation support and a number of examples.

    @techreport{RoboChart,
      title = {{R}obo{C}hart {R}eference {M}anual},
      author = {A.~Miyazawa and A.~Cavalcanti and P.~Ribeiro and W.~Li and J.~Woodcock and J.~Timmis},
      institution = {University of York},
      year = {2016},
      month = feb,
      type = {{T}echnical report},
      url = {https://www.cs.york.ac.uk/circus/publications/techreports/reports/robochart-reference.pdf}
    }
    

Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500