@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}
}
@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{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}
}
I am a research associate at the Department of Computer Science of the University of York working in the RoboCalc 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 for 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 for the EPSRC funded project hiJaC (high-integrity Java applications using Circus).
My research interests include formal semantics of graphical notations, refinement, formal specification, state-rich process algebras, Circus and Safety Critical Java.