Department of Computer Science

Publications

Papers

  • 1. 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}
    }
    
  • 2. 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}
    }
    
  • 3. 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/~alcc/publications/papers/ZOFC18.pdf}
    }
    
  • 4. 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}
    }
    
  • 5. 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/~alcc/publications/papers/CMPW17.pdf}
    }
    
  • 6. 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/~alcc/publications/papers/OCS17.pdf}
    }
    
  • 7. 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}
    }
    
  • 8. 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}
    }
    
  • 9. 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}
    }
    
  • 10. 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}
    }
    
  • 11. 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. 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{Miyazawa2016,
      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 = {http://www.cs.york.ac.uk/circus/RoboCalc/assets/RoboChart-manual.pdf}
    }
    

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