Checking JML specifications with B machines

被引：0
|
作者：
Bouquet, F [1 ]
Dadeau, F [1 ]
Groslambert, J [1 ]
机构：
[1] Univ Franche Comte, CNRS, INRIA, Lab Informat, F-25030 Besancon, France
来源：
ZB 2005: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, PROCEEDINGS | 2005年 / 3455卷
关键词：
!text type='Java']Java[!/text] Modeling language; JML; object-oriented; B method; specifications; abstract machines;
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
This paper presents a solution to the lack of tool-support for the JML models verification. We propose an approach for expressing JML specifications within the B abstract machines notation. The B machines generated from the JML can then be checked to ensure their correctness. Thus, we deduce the correctness of the original JML specification, ensured by rewriting rules which give the semantical equivalence of the two models. More generally, this translation can be applied to object-oriented specification languages using before-after predicates.
引用
收藏
页码：434 / 453
页数：20
相关论文
共 50 条
  • [1] JML2B: Checking JML specifications with B machines
    Bouquet, Fabrice
    Dadeau, Frederic
    Groslambert, Julien
    [J]. B 2007: FORMAL SPECIFICATION AND DEVELOPMENT IN B, PROCEEDINGS, 2007, 4355 : 285 - +
  • [2] Checking JML specifications using an extensible software model checking framework
    Edwin Robby
    Matthew B. Rodríguez
    John Dwyer
    [J]. International Journal on Software Tools for Technology Transfer, 2006, 8 (3) : 280 - 299
  • [3] Symbolic animation of JML specifications
    Bouquet, F
    Dadeau, R
    Legeard, B
    Utting, M
    [J]. FM 2005: FORMAL METHODS, PROCEEDINGS, 2005, 3582 : 75 - 90
  • [4] JML-Testing-Tools: A symbolic animator for JML specifications using CLP
    Bouquet, F
    Dadeau, F
    Legeard, B
    Utting, M
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2005, 3440 : 551 - 556
  • [5] Specifying and checking method call sequences in JML
    Cheon, Y
    Perumandla, A
    [J]. SERP '05: PROCEEDINGS OF THE 2005 INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING RESEARCH AND PRACTICE, VOLS 1 AND 2, 2005, : 511 - 516
  • [6] Generating JML specifications from Alloy expressions
    [J]. 1600, Springer Verlag (8855):
  • [7] JML's rich, inherited specifications for behavioral subtypes
    Leavens, Gary T.
    [J]. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2006, 4260 : 2 - 34
  • [8] Using Patterns to Map OCL Constraints to JML Specifications
    Hamie, Ali
    [J]. MODEL-DRIVEN ENGINEERING AND SOFTWARE DEVELOPMENT, MODELSWARD 2014, 2015, 506 : 35 - 48
  • [9] JML's rich, inherited specifications for behavioral subtypes
    Department of Computer Science, Iowa State University, 229 Atanasoff Hall, Ames, IA 50011-1041, United States
    [J]. Lect. Notes Comput. Sci., 2006, (2-34):
  • [10] Automated boundary test generation from JML specifications
    Bouquet, Fabrice
    Dadeau, Frederic
    Legeard, Bruno
    [J]. FM 2006: FORMAL METHODS, PROCEEDINGS, 2006, 4085 : 428 - 443
12345