Hello world!

@article{DBLP:journals/sosym/MaozR21,

title = {Spectra: a specification language for reactive systems},

author = {Shahar Maoz and Jan Oliver Ringert},

url = {https://doi.org/10.1007/s10270-021-00868-z},

doi = {10.1007/s10270-021-00868-z},

year  = {2021},

date = {2021-11-03},

journal = {Softw. Syst. Model.},

volume = {20},

number = {5},

pages = {1553--1586},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@article{Diego2021,

title = {Learning by sampling: learning behavioral family models from software product lines},

author = {Damasceno, Carlos Diego and Mousavi, Mohammad Reza and Simao, Adenilso},

year  = {2021},

date = {2021-08-18},

urldate = {2021-08-18},

journal = {Empirical Software Engineering},

volume = {26},

number = {4},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@article{FisherMRSWY21,

title = {Towards a Framework for Certification of Reliable Autonomous Systems},

author = {Michael Fisher and Viviana Mascardi and Kristin Yvonne Rozier and {Bernd-Holger} Schlingloff and Michael Winikoff and Neil {Yorke-Smith}},

url = {https://doi.org/10.1007/s10458-020-09487-2},

doi = {10.1007/s10458-020-09487-2},

year  = {2021},

date = {2021-08-12},

urldate = {2021-08-12},

journal = {Autonomous Agents and Multi Agent Systems},

volume = {35},

number = {8},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@article{MRLCTW19,

title = {RoboChart: modelling and verification of the functional behaviour of robotic applications},

author = {Alvaro Miyazawa and Pedro Ribeiro and Wei Li and Ana Cavalcanti and Jon Timmis, and Jim Woodcock},

url = {https://rdcu.be/bh7dI},

doi = {https://doi.org/10.1007/s10270-018-00710-z},

journal = {Software & Systems Modeling},

volume = {18},

number = {5},

pages = {3097-3149},

publisher = {Springer},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@article{FosterBCWoodcockZ2019,

title = {Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP},

author = {Simon Foster and James Baxter and Ana Cavalcanti and Jim Woodcock and Frank Zeyda},

url = {http://arxiv.org/abs/1905.05500},

journal = {CoRR},

volume = {abs/1905.05500},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@article{Dennis2016,

title = {Practical verification of decision-making in agent-based autonomous systems},

author = {Dennis Louise and Michael Fisher and Nicholas Lincoln and Alexei Lisitsa and Sandor Veres},

url = {https://doi.org/10.1007/s10515-014-0168-9},

doi = {10.1007/s10515-014-0168-9},

isbn = {1573-7535},

journal = {Automated Software Engineering},

volume = {23},

number = {3},

pages = {305--359},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@article{jsan10030041,

title = {A Double-Level Model Checking Approach for an Agent-Based Autonomous Vehicle and Road Junction Regulations},

author = {Gleifer Vaz Alves and Louise Dennis and Michael Fisher},

url = {https://www.mdpi.com/2224-2708/10/3/41},

doi = {10.3390/jsan10030041},

issn = {2224-2708},

journal = {Journal of Sensor and Actuator Networks},

volume = {10},

number = {3},

abstract = {Usually, the design of an Autonomous Vehicle (AV) does not take into account traffic rules and so the adoption of these rules can bring some challenges, e.g., how to come up with a Digital Highway Code which captures the proper behaviour of an AV against the traffic rules and at the same time minimises changes to the existing Highway Code? Here, we formally model and implement three Road Junction rules (from the UK Highway Code). We use timed automata to model the system and the MCAPL (Model Checking Agent Programming Language) framework to implement an agent and its environment. We also assess the behaviour of our agent according to the Road Junction rules using a double-level Model Checking technique, i.e., UPPAAL at the design level and AJPF (Agent Java PathFinder) at the development level. We have formally verified 30 properties (18 with UPPAAL and 12 with AJPF), where these properties describe the agent’s behaviour against the three Road Junction rules using a simulated traffic scenario, including artefacts like traffic signs and road users. In addition, our approach aims to extract the best from the double-level verification, i.e., using time constraints in UPPAAL timed automata to determine thresholds for the AVs actions and tracing the agent’s behaviour by using MCAPL, in a way that one can tell when and how a given Road Junction rule was selected by the agent. This work provides a proof-of-concept for the formal verification of AV behaviour with respect to traffic rules.},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@article{DennisAAAI21,

title = {Verifiable Machine Ethics in Changing Contexts},

author = {Louise A. Dennis and Martin Mose Bentzen and Felix Lindner and Michael Fisher},

url = {https://ojs.aaai.org/index.php/AAAI/article/view/17366},

journal = {Proceedings of the AAAI Conference on Artificial Intelligence},

volume = {35},

number = {13},

pages = {11470-11478},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@article{MousaviLMCS2021,

title = {Conformance Relations and Hyperproperties for Doping Detection in Time and Space},

author = {Biewer, Sebastian and Dimitrova, Rayna and Fries, Michael and Gazda, Maciej and Heinze, Thomas and Hermanns, Holger and Mousavi, Mohammad Reza },

url = {https://arxiv.org/pdf/2012.03910.pdf},

journal = {Logical Methods in Computer Science},

abstract = {    We present a novel and generalised notion of doping cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. As a formal basis for monitoring conformance-based cleanness, we develop the temporal logic HyperSTL*, an extension of Signal Temporal Logics with trace quantifiers and a freeze operator. We show that our generalised definitions are essential in a data-driven method for doping detection and apply our definitions to a case study concerning diesel emission tests. },

keywords = {},

pubstate = {forthcoming},

tppubtype = {article}

}

@article{DBLP:journals/sosym/MaozR21,

title = {Spectra: a specification language for reactive systems},

author = {Shahar Maoz and Jan Oliver Ringert},

url = {https://doi.org/10.1007/s10270-021-00868-z},

doi = {10.1007/s10270-021-00868-z},

year  = {2021},

date = {2021-11-03},

journal = {Softw. Syst. Model.},

volume = {20},

number = {5},

pages = {1553--1586},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@article{Diego2021,

title = {Learning by sampling: learning behavioral family models from software product lines},

author = {Damasceno, Carlos Diego and Mousavi, Mohammad Reza and Simao, Adenilso},

year  = {2021},

date = {2021-08-18},

urldate = {2021-08-18},

journal = {Empirical Software Engineering},

volume = {26},

number = {4},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@article{FisherMRSWY21,

title = {Towards a Framework for Certification of Reliable Autonomous Systems},

author = {Michael Fisher and Viviana Mascardi and Kristin Yvonne Rozier and {Bernd-Holger} Schlingloff and Michael Winikoff and Neil {Yorke-Smith}},

url = {https://doi.org/10.1007/s10458-020-09487-2},

doi = {10.1007/s10458-020-09487-2},

year  = {2021},

date = {2021-08-12},

urldate = {2021-08-12},

journal = {Autonomous Agents and Multi Agent Systems},

volume = {35},

number = {8},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@article{MRLCTW19,

title = {RoboChart: modelling and verification of the functional behaviour of robotic applications},

author = {Alvaro Miyazawa and Pedro Ribeiro and Wei Li and Ana Cavalcanti and Jon Timmis, and Jim Woodcock},

url = {https://rdcu.be/bh7dI},

doi = {https://doi.org/10.1007/s10270-018-00710-z},

journal = {Software & Systems Modeling},

volume = {18},

number = {5},

pages = {3097-3149},

publisher = {Springer},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@article{FosterBCWoodcockZ2019,

title = {Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP},

author = {Simon Foster and James Baxter and Ana Cavalcanti and Jim Woodcock and Frank Zeyda},

url = {http://arxiv.org/abs/1905.05500},

journal = {CoRR},

volume = {abs/1905.05500},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@article{Dennis2016,

title = {Practical verification of decision-making in agent-based autonomous systems},

author = {Dennis Louise and Michael Fisher and Nicholas Lincoln and Alexei Lisitsa and Sandor Veres},

url = {https://doi.org/10.1007/s10515-014-0168-9},

doi = {10.1007/s10515-014-0168-9},

isbn = {1573-7535},

journal = {Automated Software Engineering},

volume = {23},

number = {3},

pages = {305--359},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@article{jsan10030041,

title = {A Double-Level Model Checking Approach for an Agent-Based Autonomous Vehicle and Road Junction Regulations},

author = {Gleifer Vaz Alves and Louise Dennis and Michael Fisher},

url = {https://www.mdpi.com/2224-2708/10/3/41},

doi = {10.3390/jsan10030041},

issn = {2224-2708},

journal = {Journal of Sensor and Actuator Networks},

volume = {10},

number = {3},

abstract = {Usually, the design of an Autonomous Vehicle (AV) does not take into account traffic rules and so the adoption of these rules can bring some challenges, e.g., how to come up with a Digital Highway Code which captures the proper behaviour of an AV against the traffic rules and at the same time minimises changes to the existing Highway Code? Here, we formally model and implement three Road Junction rules (from the UK Highway Code). We use timed automata to model the system and the MCAPL (Model Checking Agent Programming Language) framework to implement an agent and its environment. We also assess the behaviour of our agent according to the Road Junction rules using a double-level Model Checking technique, i.e., UPPAAL at the design level and AJPF (Agent Java PathFinder) at the development level. We have formally verified 30 properties (18 with UPPAAL and 12 with AJPF), where these properties describe the agent’s behaviour against the three Road Junction rules using a simulated traffic scenario, including artefacts like traffic signs and road users. In addition, our approach aims to extract the best from the double-level verification, i.e., using time constraints in UPPAAL timed automata to determine thresholds for the AVs actions and tracing the agent’s behaviour by using MCAPL, in a way that one can tell when and how a given Road Junction rule was selected by the agent. This work provides a proof-of-concept for the formal verification of AV behaviour with respect to traffic rules.},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@article{DennisAAAI21,

title = {Verifiable Machine Ethics in Changing Contexts},

author = {Louise A. Dennis and Martin Mose Bentzen and Felix Lindner and Michael Fisher},

url = {https://ojs.aaai.org/index.php/AAAI/article/view/17366},

journal = {Proceedings of the AAAI Conference on Artificial Intelligence},

volume = {35},

number = {13},

pages = {11470-11478},

keywords = {},

pubstate = {published},

tppubtype = {article}

}

@article{MousaviLMCS2021,

title = {Conformance Relations and Hyperproperties for Doping Detection in Time and Space},

author = {Biewer, Sebastian and Dimitrova, Rayna and Fries, Michael and Gazda, Maciej and Heinze, Thomas and Hermanns, Holger and Mousavi, Mohammad Reza },

url = {https://arxiv.org/pdf/2012.03910.pdf},

journal = {Logical Methods in Computer Science},

abstract = {    We present a novel and generalised notion of doping cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. As a formal basis for monitoring conformance-based cleanness, we develop the temporal logic HyperSTL*, an extension of Signal Temporal Logics with trace quantifiers and a freeze operator. We show that our generalised definitions are essential in a data-driven method for doping detection and apply our definitions to a case study concerning diesel emission tests. },

keywords = {},

pubstate = {forthcoming},

tppubtype = {article}

}