Overpof.free.fr

Manuel Bernardo Barbosa - mbb@di.uminho.pt 3. Specification and validation of CANopen using PROMELA and Spin 4. Analysis of the Conformance Testing approach Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing • CANopen is a communication protocol designed for distributed control in industrial environments: system integration.
• Typical CANopen applications perform the connection of controllers (e.g. PLCs) to intelligent sensors and actuators such as I/O modulesand motion controllers: it is a field-level protocol.
• Other areas of application: medical applications, railways, maritime • Competitiveness: low cost, reliability, flexibility, diversity of CANopen- compatible products, made in Europe, European Standard EN 50325-4.
Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing • Originally developed for passenger car applications: – most European cars use CAN networks for engine management– many use it also for connecting body electronics e.g. lighting control.
– others use it for diagnostic interfacing and entertainment equipment.
• CAN features make it a good solution for industrial real-time applications: – Producer/Consumer broadcast model: message identifiers instead of station addresses. It is content-oriented.
– Message identifiers determine bus access priorities: requests are handled in the order of the importance of the messages.
– High reliability based on multi-master capabilities and data integrity – Low cost and guaranteed availability.
Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing • CAN hardware implementations provide OSI layers #1 and #2 services: – transmission of frames carrying up to 8 data bytes.
– remote data frame request.
– complex error handling mechanisms.
• CAN functionality is too low-level to be employed directly in industrial Problems such as network management, data segmentation and synchronisation must (always) be addressed.
• Higher-layer protocols are software-based communication frameworks that provide this type of functionality using CAN as a communicationlink.
• Examples: CANopen, Devicenet, CAN Kingdom.
Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing CANopen: A Three-And-A-Half Layer Protocol Device
Profiles
Communication
Application
Controller
Data Link
Physical
• The User Application implementation is constrained by Device Profiles.
This is sometimes called a User Layer.
Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing • Network configuration (potentially automatic) and network management • OO access to parameters and data block transfer (segmentation) • Device synchronisation: synchronous reading or setting of inputs, outputs • Cyclic and event-driven data transfer • Device profiles: generic I/O modules, drives and motion controllers, measuring devices and closed-loop controllers, encoders, proportionalhydraulic valves, etc.
Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing Inputs / Outputs
Object Dictionary
Application
SDO PDO NMT EMG
CAN Electronics
Data Link
Physical
CAN Network
Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing • CANopen is steered by the CAN in Automation (CiA) users group.
CANopen became an European standard in 2002.
• Important developments leading to this standardisation were: – the restructuring of the CANopen specifications (DS301 V4), and– the creation of a CANopen-compliance certification system.
• The CANopen certification system was important because: – It implies a stabilised specification whose integrity is protected by conformance testing implementations.
– It associates the CANopen brand with a culture of rigour.
– It is great publicity for complying manufacturers: offer conformance.
– It is a quality seal for users to look for: look for interoperability.
Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing • This work was carried out while the CANopen Conformance Testing • The contribution was to find answers to the following questions: – How does CANopen Conformance Testing relate to the concepts defined in the International Standard for OSI Conformance Testing ? – Can a global change in its strategy lead to an increase in its error – How does CANopen Conformance Testing rate when it is formally analysed in light of Conformance Testing theory? – Can a formal analysis and validation of the CANopen specification and associated Test Cases lead to possible enhancements? Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing Conformance Testing Communication Protocols Formal Methods
Test Suite
Test Case design
Specification
Abstraction
Instance
Dynamic Testing
Implementation
Test Tool
Under Test
Static Testing
Test Selection
Conformance Statement
Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing CANopen Conformance Testing: Remote Testing Device Profiles
Upper PCO
Accessible
Application
Lower PCO
Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing Formal Specification of CANopen using PROMELA • PROMELA is a notation for specifying the procedural rules in Communication Protocols, in order to study their structure and toverify their completeness and logical consistency [Holtzmann].
– Basic objects: processes, message channels and state variables.
– Syntax similar to C but no distinction between conditions and – Data types: bit, bool, byte, short and int; arrays and structs.
– Processes represent entities executing concurrently.
model procedures, including recursive ones.
– Communication using channels can be asynchronous or synchronous.
– Statements: if, do, break, skip, timeout.
• Correctness requirements: assertions, valid end statements (deadlocks), valid cycles (livelocks), progress statements (non-progress cycles),temporal claims.
Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing Stimulator
Stimulator
Application
Protocol
Protocol
Physical & Data
CAN Emulation Model
Link Layers
Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing do:: ((timeout)&&(NMT_Err==1)) -> DLL_to_AL[1]?message_in ->message_out.identifier=RECEIVE_A;.
NMT_Err=1;AL_to_DLL[1]!message_out; Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing Validation of the CANopen Specification using Spin Validation
Validator
Specification
Random Simulation
Validation
Guided Simulation
(Formal)
– Identification of ambiguities and inconsistencies in the specification.
– Identification of problems introduced by message loss and message – Clarification of the use of timeout mechanisms.
Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing • Objective: to establish that the control structure in an implementation complies with the control structure defined in the specification.
• Using suitable abstract models, conformance is an implementation relation between the set of implementations and the set of specifications.
• Specifications and implementations can be modeled as Finite State Machines (FSM). Implementarion relation: FSM equivalence.
• Conformance Testing is the problem of establishing whether F SMIUT is – there is complete knowledge of F SMspec,– and that F SMIUT is a black-box of which only the input and output signals are known → testing through I/O sequences Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing Test Case generation vs Test Case evaluation • Ideally it should be possible to automatically generate Test Cases from • Several methods have been proposed, but they all suffer from severe • An expert in the technology that is to be tested (seldom an expert in testing) must be involved in the Test Case generation process.
• Formal methods can be useful in assessing Test Case quality.
• One of the ways in which this can be achieved is applying reachability analysis techniques to models of Test Case execution.
Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing Test Case Evaluation Through Reachability Analysis • Set of transitions/states not reached in F SMspec, when it is stimulated according to a given Test Case: Tuncovered ⊂ T /Suncovered ⊂ S • Clearly, a Test Case does not cover all of the implementation’s and the verification performed by the Test Case is not complete.
• Defining the sets Ttarget ⊂ T and Starget ⊂ S as the set of transitions and states that the designer of the Test Case identifies as relevant in theverification of an IUT, a good Test Case implies: Smissed = Starget ∩ Suncovered = ∅ ∧ Tmissed = Ttarget ∩ Tuncovered = ∅ Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing User Layer
Model (Formal
Lower Tester
Specification)
of the IUT
Simplified model of the Lower PCO
System Under Test
Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing :: ((M_slave_state != message_in.AL_msg.state)||(toggle != message_in.AL_msg.toggle)) -> printf("Conformance Error: State"); printf("Conformance Error: Timeout"); Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing • Identification of points of execution left uncovered by Test Cases.
• Test Case simplification maintaining Test Case quality.
• Experimental trials on commercial devices demonstrate benefits.
Manuel Bernardo Barbosa - mbb@di.uminho.pt CANopen - Formal Specification and Validation - Conformance Testing

Source: http://overpof.free.fr/schneider/CAN%20&%20CANopen/CANopen/G%E9n%E9ralit%E9s/Topos/En/Manuel%20Bernardo%20Barbosa/Presentation.pdf