On the Formal Verification of Middleware Behavioral Properties

被引：6

作者：

Hugues, Jerome ^{[1
]}

Vergnaud, Thomas ^{[1
]}

Pautet, Laurent ^{[1
]}

Thierry-Mieg, Yann ^{[2
]}

Baarir, Soheib ^{[2
]}

Kordon, Fabrice ^{[2
]}

机构：

[1] CNRS, GET Telecom Paris, LTCI, UMR 5141, 46 Rue Barrault, F-75634 Paris 13, France

[2] Univ Paris 06, SRC, Lab Informat Paris 6, F-75252 Paris 05, France

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2005年 / 133卷

关键词：

Middleware design; Verification; Petri nets; LTL; Symmetries;

D O I：

10.1016/j.entcs.2004.08.062

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

Distribution middleware is often integrated as a COTS, providing distribution facilities for critical, embedded or large-scale applications. So far, typical middleware does not come with a complete analysis of their behavioral properties. In this paper, we present our work on middleware modeling and the verification of its behavioral properties; the study is applied to our middleware architecture: PolyORB. Then we present the tools and techniques deployed to actually verify the behavioral properties of our model: Petri nets, temporal logic and advanced algorithms to reduce the size of the state space. Finally, we detail some properties we verify and assess our methodology.

引用

页码：139 / 157

页数：19