CANOpen is a communication protocol and device specification used in automation system. It is a commercial protocol typically related with embedded networking. Since embedded systems are widely used in automations, CANOpen does not only exist in our daily life, but also in a variety of industries, such as household applications, automobiles, medical equipment, subsea facilities, and so on. Some of these applications are so sophisticated that they do not allow any fatal defect, like medical equipment, and some other applications are too resource-consuming to tolerate configuration delay, such as subsea platforms. Although it is not a short period since CANOpen protocol is proposed, there might still be some uncovered issues. Commercial systems tests commonly rely on the specific enviroments, which is useful to discover bugs in specific applications. But in general, it is not an efficient way to find potential issues in protocol levels. Hence, we need a method to help us solve this problem. Formal verification, providing great contributions to software and hardware system testing, is a potential method to test a protocol itself, as well, specific applications where the protocol is applied to. Maude is formal declarative formal languages based on mathematical theory of rewrite logic. Compared to traditional programming languages, a declarative language places emphasis on modeling with naturalness, ease and precision. Full Maude is an extension of Maude which adds the notation of object-oriented modeling.
In these thesis, we model some key parts of CANOpen using Full Maude, which our validation work also relies on. Since CANOpen is a complicated protocol, modeling the entire functions of CANOpen is a great task. Dividing CANOpen into two logical functions as communication and controlling parts, we focus our attention on controlling functions, which includes the Emergency Service (EMCY) and Network Management (NMT). Using Full Maude, we build the model of the controlling function based on both equation logic and rewriting logic. The resulting model is a translation from the human-language-described standard to a formal specification, with which we then do validation on to prove the soundness of parts of CANOpen.
| supervisors | Ingrid Chieh Yu |