TEST GENERATION FROM BOUNDED ALGEBRAIC SPECIFICATIONS USING ALLOY

被引：0
|
作者：
de Andrade, Francisco Rebello [1 ]
Faria, Joao Pascoal [1 ,2 ]
Paiva, Ana C. R. [1 ]
机构：
[1] Univ Porto, Fac Engn, Dept Informat Engn, Oporto, Portugal
[2] INESC Porto, P-4200465 Oporto, Portugal
来源：
ICSOFT 2011: PROCEEDINGS OF THE 6TH INTERNATIONAL CONFERENCE ON SOFTWARE AND DATABASE TECHNOLOGIES, VOL 2 | 2011年
关键词：
Test case generation; Algebraic specifications; Abstract data types; Alloy analyzer;
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
Algebraic specification languages have been successfully used for the formal specification of abstract data types (ADTs) and software components, and there are several approaches to automatically derive test cases that check the conformity between the implementation and the algebraic specification of a software component. However, existing approaches do not assure the coverage of conditional axioms and conditions embedded in complex axioms. In this paper, we present a novel approach and a tool to automatically derive test cases from bounded algebraic specifications of ADTs, assuring axiom coverage and of all minterms in its full disjunctive normal form (FDNF). The algebraic specification is first translated into the Alloy modelling language, and the Alloy Analyzer tool is used to find model instances for each test goal (axiom and minterm to cover), from which test cases in JUnit are extracted.
引用
收藏
页码：192 / 200
页数：9
相关论文
共 50 条
  • [21] LOFT: A tool for assisting selection of test data sets from algebraic specifications
    Marre, B
    [J]. TAPSOFT '95: THEORY AND PRACTICE OF SOFTWARE DEVELOPMENT, 1995, 915 : 799 - 800
  • [22] Automated generation of test programs from closed specifications of classes and test cases
    Leow, WK
    Khoo, SC
    Sun, Y
    [J]. ICSE 2004: 26TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, PROCEEDINGS, 2004, : 96 - 105
  • [23] Automatic RTL Test Generation from SystemC TLM Specifications
    Chen, Mingsong
    Mishra, Prabhat
    Kalita, Dhrubajyoti
    [J]. ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2012, 11 (02)
  • [24] Safety property driven test generation from JML specifications
    Bouquet, Fabrice
    Dadeau, Frederic
    Groslambert, Julien
    Julliand, Jacques
    [J]. FORMAL APPROACHES TO SOFTWARE TESTING AND RUNTIME VERIFICATION, 2006, 4262 : 225 - +
  • [25] Methods and methodology for an incremental test generation from SDL specifications
    Touag, A
    Rouger, A
    [J]. SDL'99: THE NEXT MILLENNIUM, 1999, : 153 - 168
  • [26] Automatic test pattern generation from high level specifications
    Hassan, S
    Wahba, A
    Badr, A
    [J]. PROCEEDINGS OF THE 46TH IEEE INTERNATIONAL MIDWEST SYMPOSIUM ON CIRCUITS & SYSTEMS, VOLS 1-3, 2003, : 1506 - 1509
  • [27] Autolink - A tool for automatic test generation from SDL specifications
    Koch, B
    Grabowski, J
    Hogrefe, D
    Schmitt, M
    [J]. 2ND IEEE WORKSHOP ON INDUSTRIAL STRENGTH FORMAL SPECIFICATION TECHNIQUES - PROCEEDINGS, 1999, : 114 - 125
  • [28] Towards TL test generation from SystemC TLM specifications
    Chen, Mingsong
    Mishra, Prabhat
    Kalita, Dhrubajyoti
    [J]. 2007 IEEE INTERNATIONAL HIGH LEVEL DESIGN VALIDATION AND TEST WORKSHOP, PROCEEDINGS, 2007, : 91 - +
  • [29] On oracles for interpreting test results against algebraic specifications
    Machado, PDL
    [J]. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, 1999, 1548 : 502 - 518
  • [30] KVEST: Automated generation of test suites from formal specifications
    Burdonov, I
    Kossatchev, A
    Petrenko, A
    Galter, D
    [J]. FM'99-FORMAL METHODS, 1999, 1708 : 608 - 621
12345