Verificação formal de sistemas discretos distribuídos. / Formal verification of distribuited discrete systems.

AUTOR(ES)

Pedro Manuel González Del Foyo

DATA DE PUBLICAÇÃO

2009

RESUMO

This work deals with the process of design and verification of complex systems, mainly real time, concurrent and distributed systems. An enumerative technique is proposed for model-checking which is capable of determining both quantitative and qualitative properties. The proposed technique detach the algorithm for labeling the formula being checked from the state space construction, allowing a better result in the verification process. This model-checking approach shows itself valuable in practical applications. This approach was first applied to systems modeled by Time Petri Nets and further extended to a unified net called GHENeSys, which includes abstraction and hierarchy concepts as well as elements for data and control interchange, called pseudo-boxes. The GHENeSys definition was modified in order to deal with systems in which temporal requirements can be expressed through delays and deadlines as in the real-time systems. The GHENeSys environment supports a refinement technique applied to both passive and active elements. Net properties like invariants, liveness, boundedness and also the validity of temporal formulas was proved to be maintained through the refinement process if some conditions are satisfied. Such characteristics are useful to deal with complex systems design. Some experiments based on well known academic articles were used to avaliate the performance of the algorithms and a case study is presented in order to compare obtained results with those obtained using the UPPAAL tool.

ASSUNTO(S)

model-checking sistemas discretos formal verification verificação formal redes de petri temporizadas verificação de modelos discrete event systems time petri nets

Documentos Relacionados

• Controle de acesso para sistemas distribuídos.
• Formal verification of systems modeled as finite state machines.
• Integration between multi-agent systems and distributed data base systems.
• Uma Abordagem, baseada em framework e na técnica de descrição formal Estelle, para o desenvolvimento de sistemas de arquivos paralelos distribuídos.
• Verificação formal de workflows com spin