Autor/Autorin: Lima Lucas
Lucas Lima is a lecturer at Departamento de Estatística e Informática of Universidade Federal Rural de Pernambuco. He holds a Ph.D. from Universidade Federal de Pernambuco. His interests are in providing formal semantics for graphical modelling languages and developing formal verification methods for model-based designs using automated techniques.
The increasing complexity of systems has led to increasing difficulty in design. For critical systems, for which safety is a major concern, early verification and validation (V&V) is recognised as a valuable approach to promote dependability. We address these issues with a refinement technique for SysML supported by tools. In this work we describe our semantics for SysML, which is defined using a state-rich process algebra called CML and implemented in a tool for automatic generation of formal models. We also show how the semantics can be used for refinement-based analysis and development. Our case studies are a leadership-election protocol, a critical component of an industrial application, and a dwarf signal, a device used to control rail traffic. Our contributions are: a set of guidelines that provide meaning to the different modelling elements of SysML used during the design of systems; the individual formal semantics for SysML activities, blocks and interactions; an integrated semantics that combines these semantics with another defined for state machines; and a framework for reasoning using refinement about systems specified by collections of SysML diagrams.
Lucas Lima is a lecturer at Departamento de Estatística e Informática of Universidade Federal Rural de Pernambuco. He holds a Ph.D. from Universidade Federal de Pernambuco. His interests are in providing formal semantics for graphical modelling languages and developing formal veri cation methods for model-based designs using automated techniques.
Über den Autor
The author achieved his bachelor's and master's at Computer Science from Universidade Federal de Campina Grande (UFCG) and Universidade Federal de Pernambuco (UFPE), respectively. He has experience in academia and industry environments, focusing on Software Engineering, acting on topics like software processes, V&V approaches and productivity.
Klappentext
The increasing complexity of systems has led to increasing difficulty in design. For critical systems, for which safety is a major concern, early verification and validation (V&V) is recognised as a valuable approach to promote dependability. We address these issues with a refinement technique for SysML supported by tools. In this work we describe our semantics for SysML, which is defined using a state-rich process algebra called CML and implemented in a tool for automatic generation of formal models. We also show how the semantics can be used for refinement-based analysis and development. Our case studies are a leadership-election protocol, a critical component of an industrial application, and a dwarf signal, a device used to control rail traffic. Our contributions are: a set of guidelines that provide meaning to the different modelling elements of SysML used during the design of systems; the individual formal semantics for SysML activities, blocks and interactions; an integrated semantics that combines these semantics with another defined for state machines; and a framework for reasoning using refinement about systems specified by collections of SysML diagrams.
