Mousavi, Mohammad Reza; Cavalcanti, Ana; Fisher, Michael; Dennis, Louise; Hierons, Rob; Kaddouh, Bilal; Law, Effie Lai-Chong; Richardson, Rob; Ringer, Jan Oliver; Tyukin, Ivan; Woodcock, Jim
Trustworthy Autonomous Systems Through Verifiability Journal Article
In: Computer, 56 (2), pp. 40-47, 2023.
@article{10042118,
title = {Trustworthy Autonomous Systems Through Verifiability},
author = {Mohammad Reza Mousavi and Ana Cavalcanti and Michael Fisher and Louise Dennis and Rob Hierons and Bilal Kaddouh and Effie Lai-Chong Law and Rob Richardson and Jan Oliver Ringer and Ivan Tyukin and Jim Woodcock},
doi = {10.1109/MC.2022.3192206},
year = {2023},
date = {2023-03-02},
journal = {Computer},
volume = {56},
number = {2},
pages = {40-47},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Baxter, James; Cavalcanti, Ana; Gazda, Maciej; Hierons, Robert M.
Testing Using CSP Models: Time, Inputs, and Outputs Journal Article
In: ACM Trans. Comput. Logic, 24 (2), 2023, ISSN: 1529-3785.
@article{10.1145/3572837,
title = {Testing Using CSP Models: Time, Inputs, and Outputs},
author = {James Baxter and Ana Cavalcanti and Maciej Gazda and Robert M. Hierons},
url = {https://doi.org/10.1145/3572837},
doi = {10.1145/3572837},
issn = {1529-3785},
year = {2023},
date = {2023-03-01},
journal = {ACM Trans. Comput. Logic},
volume = {24},
number = {2},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
abstract = {The existing testing theories for CSP cater for verification of interaction patterns (traces) and deadlocks, but not time. We address here refinement and testing based on a dialect of CSP, called tock-CSP, which can capture discrete time properties. This version of CSP has been of widespread interest for decades; recently, it has been given a denotational semantics, and model checking has become possible using a well established tool. Here, we first equip tock-CSP with a novel semantics for testing, which distinguishes input and output events: the standard models of (tock-)CSP do not differentiate them, but for testing this is essential. We then present a new testing theory for timewise refinement, based on novel definitions of test and test execution. Finally, we reconcile refinement and testing by relating timed ioco testing and refinement in tock-CSP with inputs and outputs. With these results, this paper provides, for the first time, a systematic theory that allows both timed testing and timed refinement to be expressed. An important practical consequence is that this ensures that the notion of correctness used by developers guarantees that tests pass when applied to a correct system and, in addition, faults identified during testing correspond to development mistakes.},
keywords = {},
pubstate = {published},
tppubtype = {article}
}
Pontolillo, Gabriel; Mousavi, Mohammad Reza
A Multi-Lingual Benchmark for Property-Based Testing of Quantum Programs Inproceedings
In: Proceedings of the 3rd International Workshop on Quantum Software Engineering, pp. 1–7, Association for Computing Machinery, Pittsburgh, Pennsylvania, 2023, ISBN: 9781450393355.
@inproceedings{10.1145/3528230.3528395,
title = {A Multi-Lingual Benchmark for Property-Based Testing of Quantum Programs},
author = {Gabriel Pontolillo and Mohammad Reza Mousavi},
url = {https://doi.org/10.1145/3528230.3528395},
doi = {10.1145/3528230.3528395},
isbn = {9781450393355},
year = {2023},
date = {2023-03-01},
booktitle = {Proceedings of the 3rd International Workshop on Quantum Software Engineering},
pages = {1–7},
publisher = {Association for Computing Machinery},
address = {Pittsburgh, Pennsylvania},
series = {Q-SE '22},
abstract = {We present a multi-lingual benchmark for (property-based) testing of quantum programs. We report on the methodology used to design our benchmark and the rationale behind its design decisions.Our benchmark covers three major quantum programming languages, namely Qiskit, Cirq, and Q#. We curate our benchmark from languages documentations, open source repositories, and academic papers. In order to demonstrate the common logic of the algorithms included in our benchmark, we start from an implementation in one language (often Qiskit) and produce comparable implementations in the other two languages. We produce several properties and mutants for each program as a benchmark to measure the effectiveness of property-based testing frameworks. We reflect on the high-level quantum programming concepts offered in the three languages of our benchmark and their possible impact on testability and quality assurance.},
keywords = {},
pubstate = {published},
tppubtype = {inproceedings}
}