Please use this identifier to cite or link to this item: https://hdl.handle.net/1822/79962

Full metadata record
DC FieldValueLanguage
dc.contributor.advisorPinto, Jorge Sousapor
dc.contributor.authorMiranda, Marcelopor
dc.date.accessioned2022-10-07T17:14:13Z-
dc.date.available2022-10-07T17:14:13Z-
dc.date.issued2020-01-09-
dc.date.submitted2019-12-
dc.identifier.urihttps://hdl.handle.net/1822/79962-
dc.descriptionDissertação de mestrado em Computer Sciencepor
dc.description.abstractModern 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.por
dc.description.abstractA 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.por
dc.language.isoengpor
dc.rightsopenAccesspor
dc.rights.urihttp://creativecommons.org/licenses/by-sa/4.0/por
dc.subjectFormal methodspor
dc.subjectRuntime monitoringpor
dc.subjectTemporal logicspor
dc.subjectSALTpor
dc.subjectSpeARpor
dc.subjectMétodos formaispor
dc.subjectLógicas temporaispor
dc.titleEarly validation of system requirements and designpor
dc.typemasterThesiseng
dc.identifier.tid203018265por
thesis.degree.grantorUniversidade do Minhopor
sdum.degree.grade17 valorespor
sdum.uoeiEscola de Engenhariapor
dc.subject.fosEngenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informáticapor
Appears in Collections:BUM - Dissertações de Mestrado
DI - Dissertações de Mestrado

Files in This Item:
File Description SizeFormat 
Marcelo Antonio Caridade Miranda.pdfDissertação de Mestrado645,67 kBAdobe PDFView/Open

This item is licensed under a Creative Commons License Creative Commons

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID