Details

A framework for the specification and validation of Real Time Systems using Circus Action A framework for the specification and validation of Real Time Systems using Circus Action

by Sherif, Adnan

Abstract (Summary)
Circus é uma linguagem de especificação e programação que combina CSP, Z, e construtores do Cálculo de Refinamento. A semântica de Circus está baseada na Unifying Theories of Programming (UTP). Neste trabalho estendemos um subconjunto de Circus com operadores de tempo. A nova linguagem é denominada de Circus Time Action. Propomos um modelo novo do tempo que estende o modelo da UTP, adicionando variáveis de observacão para registrar a passagem de tempo. O novo modelo é usado para dar a semântica formal de Circus Time Action. Propriedades algébricas do modelo original de Circus são validadas no novo modelo; propriedades novas são exploradas e validadas dentro do contexto de Circus Time Action. A vantagem de utilizar o padrão de unificação proposto pela UTP é poder comparare relacionar diferentes modelos. Definimos uma função de abstração, L, que faz o mapeamento das observações registradas no novo modelo (com tempo) para observações nomodelo original (sem tempo); uma função inversa, R, é também definida. O objetivo é estabelecer uma ligação formal entre o modelo novo com tempo e o modelo original da UTP. A funçãoo L e sua função inversa R formam uma conexão de Galois. Usando a função de abstração, nós introduzimos a definição de programas insenséveis ao tempo. A função de abstração permite a exploração de algumas propriedades não temporais de um programa. Apresentamos um exemplo simples para ilustrar o uso da função de abstração na validação de propriedades que não têm tempo associado. Entretanto, sistemas de tempo real têm requisitos temporais que necessitam ser validados. Neste sentido, propomos um framework para a validação de requisitos não temporais usando os dois modelos e a relação entre eles. A estrutura do framework é baseada em um processo de particionamento. Tendo como ponto de partida o programa e sua especificação escritos em Circus Time Action, aplicamos uma função sintática que gera uma forma normal do programa e sua especificação. A forma normal consiste de duas partes: a primeira é um programa sem operadores de tempo, mas com eventos que, por convenção, representam ações temporais; a segunda é uma coleção de temporizadores (timers) usados pelo programa. A composição paralela de ambas as partesé semanticamente equivalente ao programa original. Usando apenas o componente da forma normal que não envolve tempo explicitamente, mostramos que é possível raciocinarsobre propriedades de tempo no modelo não temporal; provamos formalmente a validade deste resultado. Para ilustrar o uso do framework, utilizamos um sistema de alarme simplificado como estudo de caso. Como a validação é reduzida ao modelo sem tempo, usamos a ferramenta de verficação de modelos de CSP (FDR) para realizar as provas mecanicamente. Esta é uma outra contribuição importante deste trabalho
This document abstract is also available in English.
Bibliographical Information:

Advisor:Augusto Cézar Alves Sampaio

School:Universidade Federal de Pernambuco

School Location:Brazil

Source Type:Master's Thesis

Keywords:Engenharia de Software Métodos formais - Especificação e validação CIENCIA DA COMPUTACAO

ISBN:

Date of Publication:02/20/2006

© 2009 OpenThesis.org. All Rights Reserved.