Trustworthy Autonomous Systems Verifiability Node

@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}

}

@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}

}