Introdução a métodos formais : especificação, semântica e verificação de sistemas concorrentes

Abstract

Este tutorial apresenta uma visão geral de metodos formais para a especificação, semântica e verificação de sistemas concorrentes. Um mêtodo de especificação for- mal dá uma descrição precisa de um sistema em uma notação com uma sintaxe e semântica hem definidas. Esta semântica associa um modelo matemático ao sistema que pode então ser analisado usando técnicas de verificação formal. Sào discutidos diversos métodos de especificação formal e apresenta-se cont mais detalhes o mêtodo de gramáticas de gra,fos. Para inti'oduzir os modelos semãnticos, utiliza-se sistemas de transição (uma método clássico de descriçào de sistemas seqüenciais ou concorrentes) e apresenta-se urna classificação destes modelos. Introduz-se as principais abordagens de verificação formal e discute-se o mêtodo de verificação de rriodelos. Para ilustrar todos os métodos e modelos, emprega-se corno exemplo um sistema de controle de trens.

This tutorial is an overview of formal methods for specification, semantics, and verification of concurrent systems. A formal specification method gives a precise description of a computational system in a notation with a well-defined syntax and semantics. This semantics associates a mathematical model to the system being described, and formal verification techniques may be used to analyze properties of this model. We consider several specification methods, and present in further detail the graph grammars method. To introduce the semantic mathematical models, we use transition systems (a standard framework to describe sequential and concurrent systems) and give a classification of semantic models. This tutorial introduces the main approaches to formal verification, and discusses the model checking method. The example illustrating all concepts and methods is a control system for a train network.