USING SYSML FOR IDENTIFICATION AND REFINEMENT OF MACHINERY SAFETY PROPERTIES

In the context of the development of systems subjected to strong dependability and safety properties, standards such as the IEC 61508 recommend the use of formal verification tools. In this way, conceptual and practical approaches related to computer sciences and automatic control, such as model checking, theorem proving, control synthesis, have been widely explored. However, in spite of the consensus that early phases of a system definition are the most important in ensuring that the target system will satisfy the user's requirements, most of these models and tools address the design and implementation phases where the identification and formalisation of system properties remain tricky. This machinery-dedicated paper combines system specification models supported by SysML to identify the system properties and architecture with model checker. This method is based on the refinement of system global requirements and their projection on the system components to formalise local properties to be proved by the model checker. A mechanical press case study illustrates this approach.