Formalisation of SysML design models and an analysis strategy using refinement

O aumento da complexidade dos sistemas tem levado a um aumento na dificuldade da atividade de projeto. A abordagem padrão para desenvolvimento, baseada em tentativa e erro, com testes usados em estágios avançados para identificar erros, é custosa e leva a prazos de entrega imprevisíveis. Além disto, para sistemas críticos, para os quais segurança é um conceito chave, Verificação e Validação (V&V) com antecedência é reconhecida como uma abordagem valiosa para promover confiança. Neste contexto, nós identificamos três características importantes e desejáveis de uma técnica de V&V: (i) uma linguagem de modelagem gráfica; (ii) raciocínio formal e rigoroso, e (iii) suporte automático para modelagem e raciocínio. Nós tratamos estes pontos com uma técnica de refinamento para SysML apoiada por ferramentas. SysML é uma linguagem baseada na UML para o projeto de sistemas. Ela tem se tornado um padrão de facto na área. Há uma grande disponibilidade de ferramentas de fornecedores como IBM, Atego, e Sparx Systems. Nosso trabalho se destaca de duas maneiras: ao fornecer uma semântica para refinamento e considerar uma coleção representativa de elementos do perfil UML4SysML (blocos, máquina de estados, atividades, e interações) usados de forma combinada. Nós fornecemos uma estratégia para analisar modelos de projeto especificados em SysML. Isto facilita a descoberta de problemas mais cedo durante o ciclo de vida de desenvolvimento de sistemas, reduzindo tempo e custos de produção. Neste trabalho nós descrevemos nossa semântica a qual é definida usando uma álgebra de processo rica em estado chamada CML e implementada em uma ferramenta para geração automática de modelos formais. Nós também mostramos como esta semântica pode ser usada para análise baseada em refinamento. Nossos estudos de caso são um protocolo de eleição de líder, o qual é um componente crítico de uma aplicação industrial, e um sinal anão, o qual é um dispositivo para controlar tráfego em linhas férreas. Nossas contribuições são: um conjunto de orientações que fornecem significado para os diferentes elementos de modelagem de SysML usados durante o projeto de sistemas; as semânticas formais individuais para atividades, blocos e interações de SysML; uma semântica integrada que combina estas semânticas com outra definida para máquina de estados; e um arcabouço que usa refinamento para raciocínio de sistemas especificados por coleções de diagramas SysML.The increasing complexity of systems has led to increasing difficulty in design. The standard approach to development, based on trial and error, with testing used at later stages to identify errors, is costly and leads to unpredictable delivery times. In addition, 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. In this context, we identify three important and desirable features of a V&V technique: (i) a graphical modelling language; (ii) formal and rigorous reasoning, and (iii) automated support for modelling and reasoning. We address these points with a refinement technique for SysML supported by tools. SysML is a UML-based language for systems design; it has itself become a de facto standard in the area. There is wide availability of tool support from vendors like IBM, Atego, and Sparx Systems. Our work is distinctive in two ways: a semantics for refinement and for a representative collection of elements from the UML4SysML profile (blocks, state machines, activities, and interactions) used in combination. We provide a means to analyse design models specified using SysML. This facilitates the discovery of problems earlier in the system development lifecycle, reducing time and costs of production. In this work we describe our semantics, 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