Formal verification of interactive computing systems: Opportunities and challenges

Formal verification has the potential to provide a level of evidence based assurance not possible by more traditional development approaches. For this potential to be fulfilled, its integration into existing practices must be achieved. Starting from this premise, the position paper discusses the opp...

ver descrição completa

Detalhes bibliográficos
Autor principal: Campos, José C. (author)
Outros Autores: Harrison, Michael douglas (author)
Formato: conferencePaper
Idioma:eng
Publicado em: 2019
Assuntos:
Texto completo:http://hdl.handle.net/1822/66938
País:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/66938
Descrição
Resumo:Formal verification has the potential to provide a level of evidence based assurance not possible by more traditional development approaches. For this potential to be fulfilled, its integration into existing practices must be achieved. Starting from this premise, the position paper discusses the opportunities created and the challenges faced by the use of formal verification in the analysis of critical interactive computing systems. Three main challenges are discussed: the accessibility of the modelling stage; support for expressing relevant properties; the need to provide analysis results that are comprehensible to a broad range of expertise including software, safety and human factors.