Integrating formal specification and software verification and validation

被引：0

作者：

Duke, R ^{[1
]}

Miller, T ^{[1
]}

Strooper, P ^{[1
]}

机构：

[1] Univ Queensland, Sch Informat Technol & Elect Engn, Brisbane, Qld 4072, Australia

来源：

TEACHING FORMAL METHODS, PROCEEDINGS | 2004年 / 3294卷

关键词：

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

It is not surprising that students are unconvinced about the benefits of formal methods if we do not show them how these methods can be integrated with other activities in the software lifecycle. In this paper, we describe an approach to integrating formal specification with more traditional verification and validation techniques in a course that teaches formal specification and specification-based testing. This is accomplished through a series of assignments on a single software component that involves specifying the component in Object-Z, validating that specification using inspection and a specification animation tool, and then testing an implementation of the specification using test cases derived from the formal specification.

引用

页码：124 / 139

页数：16

共 50 条

[1] Software specification, verification and validation
Shyamasundar, RK
[J]. SADHANA-ACADEMY PROCEEDINGS IN ENGINEERING SCIENCES, 1996, 21 : 123 - 123
[2] Integrating semi-formal and formal software specification techniques
Wieringa, R
Dubois, E
[J]. INFORMATION SYSTEMS, 1998, 23 (3-4) : 159 - 178
[3] Tools for formal specification, verification, and validation of requirements
Heitmeyer, C
Kirby, J
Labaw, B
[J]. COMPASS '97 - ARE WE MAKING PROGRESS TOWARDS COMPUTER ASSURANCE?, 1997, : 35 - 47
[4] End-to-End Formal Specification, Validation, and Verification Process: A Case Study of Space Flight Software
Bergue Alves, Miriam C.
Drusinsky, Doron
Michael, James Bret
Shing, Man-Tak
[J]. IEEE SYSTEMS JOURNAL, 2013, 7 (04): : 632 - 641
[5] Testing-Based Formal Verification for Theorems and Its Application in Software Specification Verification
Liu, Shaoying
[J]. TESTS AND PROOFS, TAP 2016, 2016, 9762 : 112 - 129
[6] Formal Validation and Verification of a Medical Software Critical Component
Arcaini, Paolo
Bonfanti, Silvia
Gargantini, Angelo
Mashkoor, Atif
Riccobene, Elvinia
[J]. 2015 ACM/IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CODESIGN (MEMOCODE), 2015, : 80 - 89
[7] Formal Specification and Automated Verification of Railway Software with Frama-C
Prevosto, Virgile
Burghardt, Jochen
Gerlach, Jens
Hartig, Kerstin
Pohl, Hans
Voellinger, Kim
[J]. 2013 11TH IEEE INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN), 2013, : 710 - 715
[8] A FRAMEWORK FOR INTEGRATING FORMAL SPECIFICATION, REVIEW, AND TESTING TO ENHANCE SOFTWARE RELIABILITY
Liu, Shaoying
Tamai, Tetsuo
Nakajima, Shin
[J]. INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 2011, 21 (02) : 259 - 288
[9] Formal specification and verification of VHDL
Bickford, M
Jamsek, D
[J]. FORMAL METHODS IN COMPUTER-AIDED DESIGN, 1996, 1166 : 310 - 326
[10] Formal Specification and Verification of CRDTs
Zeller, Peter
Bieniusa, Annette
Poetzsch-Heffter, Arnd
[J]. FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, 2014, 8461 : 33 - 48

← 1 2 3 4 5 →