Efficient mechanised analysis of infinite CSPz specifications: strategy and tool support

AUTOR(ES)

Adalberto Cajueiro de Farias

DATA DE PUBLICAÇÃO

2003

RESUMO

In concurrent systems modelling, the use of different formal languages has been an alternative very used in the last years. Process algebras (like CSP and CCS) are adequate to model behaviour, while languages based on mathematical models (like Z and VDM) are more suitable to describe data aspects. Integrated languages have appeared in order to provide support to deal with different aspects at the same time. Many of them were proposed to specify concurrent, systems. CSPz, for example, is an integrated notation which makes use of CSP and Z to specify behaviour and data orthogonally. lts semantics was defined in terms of CSP, what made possible to reuse FDR, the standard CSP model checker, in CSPz verification. Although this strategy eliminates the necessity of implementing a model checker specific for CSPz, it is not sufficient to solve a problem known as state explosion. Such a problem occurs because the technique of model checking analyses all possible states of the system. lf the state space is infinite or too large, the application of model checking becomes impossible or impractical

ASSUNTO(S)

csp - Ãlgebra de processo e z - linguagem baseada em modelos matemÃticos cspz - notaÃÃo integrada que faz uso do csp engenharia nuclear abstraÃÃo de dados para cspz

Documentos Relacionados

• Abstraction of infinite and communicating CSPZ processes
• Validação de especificações de sistemas reativos: Definição e análise de critérios de teste.
• Rapid synthesis of oligodeoxyribonucleotides VI. Efficient, mechanised synthesis of heptadecadeoxyribonucleotides by an improved solid phase phosphotriester route.
• ArcAngel: a Tactic Language For Refinement and its Tool Support
• Efficient integration of artificial transposons into plasmid targets in vitro: a useful tool for DNA mapping, sequencing and genetic analysis.