Alexios Lekidis, Marius Bozga, Saddek Bensalem
Rigorous Modeling and Validation of CANopen Systems (2014)
Rigorous Modeling and Validation of CANopen Systems (2014)
TR-2014-1.pdf
Keywords: Model-based development, Networked embedded systems, Fieldbus protocols, Performance evaluation, Formal validation
Abstract: CANopen is an increasingly popular protocol for the design of networked embedded systems. Nonetheless, the large variety of communication and network management functionalities supported in it can increase significantly systems complexity and in turn, the needs for system validation at design time. We present hereafter a novel approach relying on modeling and verification techniques, allowing to provide a comprehensive and faithful analysis of CANopen systems. This approach uses BIP, a formal framework for modeling, analysis and implementation of real-time, heterogeneous, component-based systems and the associated BIP tools for simulation, performance evaluation and statistical model-checking. As a proof of concept, the approach has been applied in an existing benchmark simulating a realistic automotive system and the Pixel Detector Control System of the ATLAS experiment at CERN's Large Hadron Collider (LHC) particle accelerator. This work facilitates the systematical development of such systems and reveals potential application for the generation of optimal device configurations.
