Encontrados 4 documentos, a visualizar página 1 de 1
An approach to model checking Ada programs
Faria, José Miguel; Martins, J.; Pinto, Jorge SousaThis paper describes a tool-supported method for the formal verification of Ada programs. It presents ATOS, a tool that automati- cally extracts a model in SPIN from an Ada Program, together with a set of properties that state the correctness of the model. ATOS is also capable of extracting properties from user-provided annotations in Ada programs, inspired by the Spark Annotation language. The goal of ATOS is ...
Formal development of solutions for real-time operating systems with TLA+/TLC
Faria, José Miguel SampaioTese de mestrado. Engenharia Electrotécnica e de Computadores. Faculdade de Engenharia. Universidade do Porto. 208
Hybrid specification of reactive systems : an institutional approach
Madeira, A.; Faria, José Miguel; Martins, Manuel A.; Barbosa, L. S.This paper introduces a rigorous methodology for requirements specification of systems that react to external stimulus by evolving through different operational modes. In each mode different functionalities are provided. Starting from a classical state-machine specification, the envisaged methodology interprets each state as a different mode of operation endowed with an algebraic specification of the correspond...
On requirements engineering for reactive systems : a formal methodology
Madeira, A.; Faria, José Miguel; Martins, Manuel A.; Barbosa, L. S.This paper introduces a rigorous methodology for requirements specification of systems that react to external stimulus and consequently evolve through different operational modes, providing, in each of them, different functionalities. The proposed methodology proceeds in three stages, enriching a simple state- machine with local algebraic specifications. It resorts to an expressive variant of hybrid logic which...
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||