Publication Type

Conference Proceeding Article

Version

acceptedVersion

Publication Date

3-2020

Abstract

Cyber Physical Systems (CPSs) comprise sensors and actuators which interact with the physical environment over a computer network to achieve some control objective. Bugs in CPSs can have severe consequences as CPSs are increasingly deployed in safety-critical applications. Debugging CPSs is therefore an important real world problem. Traces from a CPS can be lengthy and are usually linked to different parts of the system, making debugging CPSs a complex and time-consuming undertaking. It is challenging to isolate a component without running the whole CPS. In this work, we propose a model-based approach to debugging a CPS. For each CPS property, active automata learning is applied to learn a fault model, which is a Deterministic Finite Automata (DFA) of the violation of the property. The L* algorithm (L*) will find a minimum DFA given the queries and counterexamples. Short test cases can then be easily extracted from the DFA and executed on the actual CPS for bug rectification.

This is a black-box approach which does not require access to the PLC source code, making it easy to apply in practice. Where source code is available, the bug can be rectified. We demonstrate the ease and effectiveness of this approach by applying it to a commercially supplied miniature lift controlled by a Programmable Logic Controller (PLC). Two bugs were discovered in the supplier code. Both of them were patched with relative ease using the models generated. We then created 20 mutated versions of the patched code and applied our approach to these mutants. Our prototype implementation successfully built at least one model for each mutant corresponding to the property violated, demonstrating its effectiveness.

Keywords

Active automata learning, Debugging, L* algorithm, Programmable logic controllers

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Formal methods and software engineering: 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, March 1-3: Proceedings

Volume

12531

First Page

147

Last Page

162

ISBN

9783030634056

Identifier

10.1007/978-3-030-63406-3_9

Publisher

Springer

City or Country

Cham

Embargo Period

7-8-2021

Copyright Owner and License

Authors

Additional URL

https://doi.org/10.1007/978-3-030-63406-3_9

Download

Share

COinS