Application of formal methods for validation and verification of embedded system communication protocol

摘要

There are plethora of control based embedded systems installed in domestic electronic systems. The correct working of these embedded systems is important for successful functionality of the overall system. Most of these embedded system communicate using some communication protocol. Thus the protocol must be error free for successful working of overall system. This paper explains a scenario in which a communication problem occurred between two embedded components. By taking the problem in to account, the paper provides formal verification techniques to solve this communication issue. Buffers are used to read and send data for inter components communication. In some situations, when data is read from the buffers without flushing them, usually junk data is induced along with information(packets) which causes the system to be in indeterminate state. This situation might result to be a complete system failure for such critical real time systems. This paper claims that such communication problems can be easily detected by developing formal models of the communication protocol and applying formal verification tests to confirm a certain property holds or not. In case of a failure, the model checker automatically generates a trace explaining how and why the property has failed. We later confirmed our results by manually generating the scenario generated by model checker in actual code. This has been an efficient bug hunting technique and we aim to test more communication protocols in future using this technique using formal methods which is a very powerful technique for validation and verification of software system problems.