Early validation of system requirements and design

Abstract

Modern society is relying more and more on electronic devices, most of which are em bedded systems and are sometimes responsible for performing safety-critical tasks. As the complexity of such systems increases due to concurrency concerns and real-time con straints, their design is more prone to errors which can lead to catastrophic outcomes. In order to reduce the risk of such outcomes, a model-based methodology is commonly used. The model describes the behaviour of the system and is subject to verification tech niques such as simulation and model checking in order to verify it behaves according to the requirements. Common problems that arise with this methodology is the ambiguity of requirements written in natural language and the translation of a requirement to a property that can be verified along with the model. This thesis proposes a tool that, after the translation of the requirements to temporal formalism, allows the automatic generation of monitors in order to verify the model. Our target platform is Simulink, which is widely used in this domain to model, simulate and analyze dynamic systems.

A sociedade de hoje depende cada vez mais de dispositivos eletrónicos, a maioria dos quais são sistemas embebidos e, por vezes, responsáveis pela realização de tarefas críticas. À medida que a complexidade destes sistemas aumenta devido a problemas de concorrência ou restrições de tempo real, o design torna-se mais suscetível a erros que podem levar a resultados catastróficos. A fim de reduzir estes riscos, recorre-se a uma metodologia de desenvolvimento baseada em modelos. O modelo descreve o comportamento do sistema e pode ser sujeito a técnicas de verificação, tais como simulação ou model checking, a fim de verificar que este exibe o comportamento descrito nos requisitos. Problemas comuns que surgem com esta metodologia devem-se a ambiguidade dos requisitos, tipicamente escritos em linguagem natural, e a tradução destes para uma propriedade que pode ser verificada em conjunto com o modelo. Esta dissertação propõe uma ferramenta que, após a tradução dos requisitos para uma linguagem de especificação formal, permite a geração automática de monitores para verificar o modelo. A plataforma para a qual os monitores são gerados e o Simulink, que é tipicamente utilizado neste domínio para modelar, simular e analisar sistemas dinâmicos.