Alvaro Miyazawa

Department of Computer Science, University of York


I am a lecturer in the Department of Coputer Science of the University of York working in the Software Engineering for Robotics Group.

My PhD developed a formal semantics for Stateflow charts and a semi-automated strategy for the verification of sequential and parallel implementations. My research focus in on formal diagrammatic and textual domain specific languages, formal verification strategies, formal refinement, applied formal methods, and formal modelling and analysis different modelling paradigms.

In the EC FP7 project Compass (Comprehensive Modelling for Advanced Systems of Systems), I have worked on modelling and analysis of Systems of Systems, in the EPSRC funded project hiJaC (high-integrity Java applications using Circus), my work focused on the design of a specification notation and verification strategy for safety critical java (SCJ) programs. In the EPSRC funded project RoboCalc, I designed and specified the RoboChart notations and its formal semantics, developed RoboTool to support modelling, analysis and verification of RoboChart models, and developed a modelling language (and its semantics) for the specification of the physical components of a robotic system. In the EPSRC funded project RoboTest, I work on the automatic code generation for RoboSim models, generation of simulations for testing, automated testing, and mutation testing approaches based on the physical models.

My research interests include formal semantics of graphical and textual languages, refinement, verification, formal specification, (state-rich) process algebras, hybrid and probabilistic modelling, Circus, formal methods and software engieering for Robotics, and Safety Critical Java.