Using Assertions to Enhance the Correctness of Kmelia Components and their Assemblies

被引：2
|
作者：
Andre, Pascal [1 ]
Ardourel, Gilles [1 ]
Attiogbe, Christian [1 ]
Lanoix, Arnaud [1 ]
机构：
[1] Univ Nantes, CNRS, LINA, UMR 6241, 2 Rue Houssiniere, F-44322 Nantes, France
来源：
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2010年 / 263卷
关键词：
Component; Assembly; Datatype; Assertions; Property Verification;
D O I：
10.1016/j.entcs.2010.05.002
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
The Kmelia component model is an abstract formal component model based on services. It is dedicated to the specification and development of correct components. This work enriches the Kmelia language to allow the description of data, expressions and assertions when specifying components and services. The objective is to enable the use of assertions in Kmelia in order to support expressive service descriptions, to support client/supplier contracts with pre/post-conditions, and to enhance formal analysis of component-based systems. Assertions are used to perform analysis of services, component assemblies and service compositions. Additionally we enable the definition of virtual contexts for required services and the corresponding observable state space for the components which provide the services. We illustrate the work with the verification of consistency properties involving data at component and assembly levels.
引用
收藏
页码：5 / 30
页数：26
相关论文
共 50 条
  • [1] Modal Assertions for Actor Correctness
    Gordon, Colin S.
    [J]. PROCEEDINGS OF THE 9TH ACM SIGPLAN INTERNATIONAL WORKSHOP ON PROGRAMMING BASED ON ACTORS, AGENTS, AND DECENTRALIZED CONTROL (AGERE '19), 2019, : 11 - 20
  • [2] Composing components with shared services in the Kmelia model
    Andre, Pascal
    Ardourel, Gilles
    Attiogbe, Christian
    [J]. SOFTWARE COMPOSITION, 2008, 4954 : 125 - 140
  • [3] Partial correctness assertions provable in dynamic logics
    Leivant, D
    [J]. FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS, 2004, 2987 : 304 - 317
  • [4] Indexed and fibered structures for partial and total correctness assertions
    Wolter, U. E.
    Martini, A. R.
    Haeusler, E. H.
    [J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2022, 32 (09) : 1145 - 1175
  • [5] Integrating Statechart Assertions into Java']Java Components Using AspectJ
    Drusinsky, Doron
    Michael, James Bret
    Otani, Thomas W.
    Shing, Man-Tak
    [J]. 2008 IEEE INTERNATIONAL CONFERENCE ON SYSTEM OF SYSTEMS ENGINEERING (SOSE), 2008, : 366 - 372
  • [6] Environment-Bound SAML Assertions: A Fresh Approach to Enhance the Security of SAML Assertions
    Chen, Kai
    Lin, Dongdai
    Yan, Li
    Sun, Xin
    [J]. INFORMATION SECURITY AND CRYPTOLOGY, INSCRYPT 2013, 2014, 8567 : 361 - 376
  • [7] Using assertions with trace
    Nazimek, Piotr
    [J]. PHOTONICS APPLICATIONS IN ASTRONOMY, COMMUNICATIONS, INDUSTRY, AND HIGH-ENERGY PHYSICS EXPERIMENTS 2015, 2015, 9662
  • [8] Assemblies of software components
    Jiang, Jianmin
    Xiao, Ying
    Zhu, Hengliang
    Zhou, Shuming
    [J]. 2009 WRI WORLD CONGRESS ON SOFTWARE ENGINEERING, VOL 3, PROCEEDINGS, 2009, : 311 - 315
  • [9] Temporal Assertions using AspectJ
    Stolz, Volker
    Bodden, Eric
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 144 (04) : 109 - 124
  • [10] ELECTRONICA HIGHLIGHTS COMPONENTS, ASSEMBLIES
    GOSCH, J
    FLETCHER, P
    [J]. ELECTRONIC DESIGN, 1990, 38 (20) : 37 - 39
12345