@article{0af446aa7f424d8f8f8b1e0ccbd7f007, title = "Probabilistic Modelling and Verification using RoboChart and PRISM", abstract = "RoboChart is a timed domain-specific language for robotics, distinctive in its support for automated verification by model checking and theorem proving. Since uncertainty is an essential part of robotic systems, we present here an extension to RoboChart to model uncertainty using probabilism. The extension enriches RoboChart state machines with probability through a new construct: probabilistic junctions as the source of transitions with a probability value. RoboChart has an accompanying tool, called RoboTool, for modelling and verification of functional and real-time behaviour. We present here also an automatic technique, implemented in RoboTool, to transform a RoboChart model into a PRISM model for verification. We have extended the property language of RoboTool so that probabilistic properties expressed in temporal logic can be written using controlled natural language.", keywords = "State machines, formal semantics, model transformation, PRISM, probabilistic model checking, domain-specific language for robotics", author = "Kangfeng Ye and Ana Cavalcanti and Simon Foster and Alvaro Miyazawa and Jim Woodcock", note = "This is an author-produced version of the published paper. Uploaded in accordance with the publisher{\textquoteright}s self-archiving policy. Further copying may not be permitted; contact the publisher for details ", year = "2021", month = jul, day = "20", language = "English", journal = "Software and Systems Modeling", issn = "1619-1366", publisher = "Springer", url = {https://rdcu.be/cyKUe} } @inbook{CBBCFMRS21, author = {A. L. C. Cavalcanti and W. Barnett and J. Baxter and G. Carvalho and M. C. Filho and A. Miyazawa and P. Ribeiro and A. C. A. Sampaio}, editor = {A. L. C. Cavalcanti and B. Dongol and R. Hierons and J. Timmis and J. C. P. Woodcock}, chapter = {RoboStar Technology: A Roboticist's Toolbox for Combined Proof, Simulation, and Testing}, title = {Software Engineering for Robotics}, year = {2021}, publisher = {Springer International Publishing}, pages = {249--293}, doi = {10.1007/978-3-030-66494-7_9}, url = {www-users.cs.york.ac.uk/ alcc/publications/papers/CBBCFMRS21.pdf} } @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}, pages = {3097–3149}, volume = {18}, issn = {1619-1374}, doi = {10.1007/s10270-018-00710-z}, url = {https://doi.org/10.1007/s10270-018-00710-z} } @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}, pages = {140-176}, volume = {181}, 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} } @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} } @inproceedings{RMLCT17, 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/ alcc/publications/papers/RMLCT17.pdf} } @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} } @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} } @Inbook{Li2018, author="Li, Wei and Miyazawa, Alvaro and Ribeiro, Pedro and Cavalcanti, Ana and Woodcock, Jim and Timmis, Jon", editor="Groß, Roderich and Kolling, Andreas and Berman, Spring and Frazzoli, Emilio and Martinoli, Alcherio and Matsuno, Fumitoshi and Gauci, Melvin", chapter="From Formalised State Machines to Implementations of Robotic Controllers", title="Distributed Autonomous Robotic Systems: The 13th International Symposium", year="2018", publisher="Springer International Publishing", address="Cham", pages="517--529", abstract="ControllersLi, Weifor autonomousMiyazawa, Alvarorobotic systemsRibeiro, Pedrocan beCavalcanti, AnaspecifiedWoodcock, Jimusing state machinesTimmis, Jon. 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 a tool to automatically create code from the state machines, establishing a rigorous connection between specification and implementation. In RoboChart, a 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.", isbn="978-3-319-73008-0", doi="10.1007/978-3-319-73008-0_36", url="https://doi.org/10.1007/978-3-319-73008-0_36" } @Inbook{Cavalcanti2017, author="Cavalcanti, A. and Miyazawa, A. and Payne, R. and Woodcock, J.", editor="Mazzara, M. and Meyer, B.", chapter="Sound Simulation and Co-simulation for Robotics", title="Present and Ulterior Software Engineering", year="2017", publisher="Springer International Publishing", address="Cham", pages="173--194", abstract="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.", isbn="978-3-319-67425-4", doi="10.1007/978-3-319-67425-4_11", url="https://doi.org/10.1007/978-3-319-67425-4_11" } @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 = {IEEE/RSJ International Conference on Intelligent Robots and Systems}, volume = {}, number = {}, pages = {3869-3876}, doi = {10.1109/IROS.2017.8206238}, url = {www-users.cs.york.ac.uk/ alcc/publications/papers/MRLCT17.pdf} } @inproceedings{CMWWZ17, booktitle = {Engineering Trustworthy Software Systems}, title = {{Java in the Safety-Critical Domain}}, author = {A. L. C. Cavalcanti and A. Miyazawa and A. Wellings and J. C. P. Woodcock and S. Zhao}, year = {2017}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, editor = {J. Bowen and Z. Liu and Z. Zhang}, pages = {110-150}, doi = {10.1007/978-3-319-56841-6_4}, url = {https://www-users.cs.york.ac.uk/ alcc/publications/papers/CMWWZ17.pdf}, volume = 10215 } @Inproceedings{Miyazawa2016, author="A. Miyazawa and A. Cavalcanti", editor="Corn{\'e}lio, M{\'a}rcio and Roscoe, Bill", title="Refinement Strategies for Safety-Critical Java", booktitle="Formal Methods: Foundations and Applications: 18th Brazilian Symposium, SBMF 2015, Belo Horizonte, Brazil, September 21-22, 2015, Proceedings", year="2016", publisher="Springer International Publishing", address="Cham", pages="93--109", isbn="978-3-319-29473-5", doi="10.1007/978-3-319-29473-5_6", url="https://www.cs.york.ac.uk/circus/publications/papers/Miyazawa2015a.pdf" } @Inproceedings{EPTCS209.6, author = "A. Miyazawa and A. Cavalcanti", year = "2016", title = "SCJ-Circus: a refinement-oriented formal notation for Safety-Critical Java", editor = "Derrick, John and Boiten, Eerke and Reeves, Steve", booktitle = "{Proceedings 17th International Workshop on} Refinement, {Oslo, Norway, 22nd June 2015}", series = "Electronic Proceedings in Theoretical Computer Science", volume = "209", publisher = "Open Publishing Association", pages = "71-86", doi = "10.4204/EPTCS.209.6", url = "https://www.cs.york.ac.uk/circus/publications/papers/Miyazawa2015.pdf" } @Article{Lima2015, author="L. Lima and A. Miyazawa and A. Cavalcanti and M. Corn{\'e}lio and J. Iyoda and A. Sampaio and R. Hains and A. Larkham and V. Lewis", title="An integrated semantics for reasoning about SysML design models using refinement", journal="Software {\&} Systems Modeling", year="2015", pages="1--28", volume="online first", abstract="SysML is a variant of UML for systems design. Several formalisations of SysML (and UML) are available. Our work is distinctive in two ways: a semantics for refinement and for a representative collection of elements from the UML4SysML profile (blocks, state machines, activities, and interactions) used in combination. We provide a means to analyse and refine design models specified using SysML. This facilitates the discovery of problems earlier in the system development lifecycle, reducing time, and costs of production. Here, we describe our semantics, which is defined using a state-rich process algebra and implemented in a tool for automatic generation of formal models. We also show how the semantics can be used for refinement-based analysis and development. Our case study is a leadership-election protocol, a critical component of an industrial application. Our major contribution is a framework for reasoning using refinement about systems specified by collections of SysML diagrams.", issn="1619-1374", doi="10.1007/s10270-015-0492-y", url="publications/LMCCISHLL15.pdf", } @InProceedings{FosterMWCFL14, Title = {An approach for managing semantic heterogeneity in Systems of Systems Engineering}, Author = {S. Foster and A. Miyazawa and J. C. P. Woodcock and A. L. C. Cavalcanti and J. S. Fitzgerald and P. G. Larsen}, Booktitle = {9th International Conference on System of Systems Engineering, SoSE 2014, Glenelg, Australia, June 9-13, 2014}, Year = {2014}, Pages = {113-118}, Publisher = {{IEEE}}, URL = {https://www-users.cs.york.ac.uk/ alvarohm/publications/sose-utphet.pdf}, Owner = {Alvaro}, Timestamp = {2015.09.29} } @InProceedings{BFPMK14, Title = {{SysML contracts for systems of systems}}, Author = {J. Bryans and J. Fitzgerald and R. Payne and A. Miyazawa and K. Kristensen}, Booktitle = {9th International Conference on System of Systems Engineering, SoSE 2014, Glenelg, Australia, June 9-13, 2014}, Year = {2014}, Pages = {73-78}, Publisher = {{IEEE}}, URL = {https://www-users.cs.york.ac.uk/ alvarohm/publications/sose-contracts.pdf}, Owner = {Alvaro}, Timestamp = {2015.09.29}, doi={10.1109/SYSOSE.2014.6892466} } @InProceedings{HMCK14, Title = {{Assurance Cases for Block-configurable Software}}, Author = {R. Hawkins and A. Miyazawa and A. L. C. Cavalcanti and T. Kelly}, Booktitle = {33rd International Conference on Computer Safety, Reliability and Security}, Year = {2014}, Publisher = {Springer}, Series = {Lecture Notes in Computer Science}, Pages = {155-169}, Owner = {Alvaro}, Timestamp = {2015.09.29}, URL = {https://www-users.cs.york.ac.uk/ alcc/publications/papers/HMCKR14.pdf} } @InProceedings{Miyazawa2014b, Title = {Formal Refinement in SysML}, Author = {A. Miyazawa and A. L. C. Cavalcanti}, Booktitle = {IFM}, Publisher = {Springer}, Year = {2014}, Editor = {Albert, E. and Sekerinski, E.}, Pages = {155-170}, Series = {LNCS}, Volume = {8739}, Comment = {[pdf]}, DOI = {10.1007/978-3-319-10181-1_10}, ISBN = {978-3-319-10180-4}, Language = {English}, Owner = {Alvaro}, Timestamp = {2015.09.29}, Url = {https://www.cs.york.ac.uk/circus/publications/papers/Miyazawa2014b.pdf} } @Article{Miyazawa2014a, Title = {Refinement-based verification of implementations of Stateflow charts}, Author = {A. Miyazawa and A. L. C. Cavalcanti}, Journal = {Formal Aspects of Computing}, Year = {2014}, Number = {2}, Pages = {367-405}, Volume = {26}, Comment = {[pdf]}, Doi = {10.1007/s00165-013-0291-6}, ISSN = {0934-5043}, Keywords = {Simulink; Z; CSP; Tactics of refinement}, Language = {English}, Owner = {Alvaro}, Publisher = {Springer London}, Timestamp = {2015.09.29}, Url = {https://www.cs.york.ac.uk/circus/publications/papers/Miyazawa2014a.pdf} } @article{Miyazawa20121151, title = "Refinement-oriented models of Stateflow charts ", journal = "Science of Computer Programming ", volume = "77", number = "10–11", pages = "1151 - 1177", year = "2012", note = "AVoCS'09 ", issn = "0167-6423", doi = "http://dx.doi.org/10.1016/j.scico.2011.07.007", url = "https://www.cs.york.ac.uk/circus/publications/papers/Miyazawa2012a.pdf", author = "A. Miyazawa and A. Cavalcanti", keywords = "Simulink", keywords = "Circus", keywords = "Formal semantics", keywords = "Verification", keywords = "Tools ", abstract = "Simulink block diagrams are widely used in industry for specifying control systems, and of particular interest and complexity are Stateflow blocks, which are themselves defined by separate charts. To make formal reasoning about diagrams and charts possible, we need to formalise their semantics; for the formal verification of their implementations, a refinement-based semantics is appropriate. An extensive subset of Simulink has been formalised in a language for refinement, namely, Circus, and here, we propose an approach to cover Stateflow charts. Our models are distinctive in their operational nature, which closely reflects the informal description of the Stateflow (simulation) semantics. We describe, formalise, and automate a strategy to generate our Circus models. The result is a solid foundation for reasoning based on refinement. " } @inproceedings{DBLP:journals/corr/abs-1106-4094, author = {A. Miyazawa and A. Cavalcanti}, title = {Refinement-based verification of sequential implementations of Stateflow charts}, booktitle = {Proceedings 15th International Refinement Workshop, Refine 2011, Limerick, Ireland, 20th June 2011.}, pages = {65-83}, year = {2011}, crossref = {DBLP:journals/corr/abs-1106-3488}, url = {https://www.cs.york.ac.uk/circus/publications/papers/Miyazawa2011a.pdf}, doi = {10.4204/EPTCS.55.5}, timestamp = {Mon, 28 Oct 2013 16:56:55 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1106-4094}, bibsource = {dblp computer science bibliography, http://dblp.org}, Owner = {Alvaro}, Timestamp = {2015.09.29} } @InProceedings{Miyazawa2013a, Title = {Formal Models of SysML Blocks}, Author = {A. Miyazawa and L. Lima and A. L. C. Cavalcanti}, Booktitle = {Formal Methods and Software Engineering}, Year = {2013}, Editor = {Groves, L. and Sun, J.}, Pages = {249-264}, Publisher = {Springer}, Series = {LNCS}, Volume = {8144}, Doi = {10.1007/978-3-642-41202-8_17}, ISBN = {978-3-642-41201-1}, Keywords = {CML; SysML; process algebra; refinement; semantics}, Language = {English}, Owner = {Alvaro}, Timestamp = {2015.09.29}, Url = {https://www.cs.york.ac.uk/circus/publications/papers/Miyazawa2013a.pdf} } @InProceedings{WCFLMP12, Title = {{Features of CML: a Formal Modelling Language for Systems of Systems}}, Author = {J. C. P. Woodcock and A. L. C. Cavalcanti and J. Fitzgerald and P. G. Larsen and A. Miyazawa and S. Perry}, Booktitle = {7th International Conference on Systems of Systems Engineering}, Year = {2012}, Publisher = {IEEE}, Series = {IEEE Systems Journal}, Volume = {6}, Pages = {1-6}, Owner = {Alvaro}, Timestamp = {2015.09.29}, url = {https://www-users.cs.york.ac.uk/ alvarohm/publications/SOSE-2012-features-of-CML.pdf} } @InProceedings{WCFLMP12, Title = {{COMPASS tool vision for a system of systems Collaborative Development Environment}}, Author = {J. W. Coleman and A. K. Malmos and P. G. Larsen and J. Peleska and R. Hains and Z. Andrews and R. Payne and S. Foster and A. Miyazawa and C. Bertolini and A. Didier}, Booktitle = {7th International Conference on Systems of Systems Engineering}, Year = {2012}, Publisher = {IEEE}, Pages = {451-456}, Owner = {Alvaro}, Timestamp = {2015.09.29}, doi={10.1109/SYSoSE.2012.6384150}, url = {https://www-users.cs.york.ac.uk/ alvarohm/publications/SoSToolsVision.pdf} }

Alvaro Miyazawa

Department of Computer Science, University of York

Publications

I am a research associate at the Departments of Electronic Engineering and Computer Science of the University of York working in the RoboTest project.

I have finished my PhD in 2012 at the University of York with a thesis entitled "Formal verification of implementations of Stateflow charts". From 2012 to 2014, I worked in the EC FP7 project Compass (Comprehensive Modelling for Advanced Systems of Systems) on modelling and analysis of Systems of Systems. From 2014 to 2015, I worked in the EPSRC funded project hiJaC (high-integrity Java applications using Circus). From 2015 to 2020, I worked in the EPSRC funded project RoboCalc.

My research interests include formal semantics of graphical notations, refinement, verification, formal specification, state-rich process algebras, Circus, formal methods and software engieering for Robotics, and Safety Critical Java.