Formal Specification of Component-Based Software Architectures: Correctness Checking (with Parq) - Calculus

被引：0

作者：

Diosa, Henry Alberto ^{[1
]}

Diaz Frias, Juan Francisco ^{[1
]}

Gaona Cuevas, Carlos Mauricio ^{[1
]}

机构：

[1] Univ Los Andes, Bogota, Colombia

来源：

REVISTA CIENTIFICA | 2010年 / 12期

关键词：

Reference architecture; reference model; rho(arq) - Calculus; formal method; software components; labelled transition systems; correctness checking; observation equivalence;

D O I：

暂无

中图分类号：

G40 [教育学];

学科分类号：

040101 ; 120403 ;

摘要：

In this paper we describe a correctness checking formal method of reference architectures against reference models in a component-based software development perspective. These models are specified by means of rho(arq)-calculus. We use two formal tools; the first, the concept of Labelled Transition System (LTS) enhanced with the conditional-transition concept for logical variables whose resolution may be obtained from a global store of constraints. The second, the observation equivalence theory proposed by Robin Milner and his collaborators in Cambridge University.

引用

页码：156 / 171

页数：16