Integrating Pattern-based Formal Requirements Specification in an Industrial Tool-chain

被引：13

作者：

Filipovikj, Predrag ^{[1
]}

Jagerfield, Trevor ^{[1
]}

Nyberg, Mattias ^{[1
]}

Rodriguez-Navas, Guillermo ^{[1
]}

Seceleanu, Cristina ^{[1
]}

机构：

[1] Malardalen Univ, Vasteras, Sweden

来源：

PROCEEDINGS 2016 IEEE 40TH ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE WORKSHOPS (COMPSAC), VOL 2 | 2016年

关键词：

D O I：

10.1109/COMPSAC.2016.140

中图分类号：

TP39 [计算机的应用];

学科分类号：

081203 ; 0835 ;

摘要：

The lack of formal system specifications is a major obstacle to the widespread adoption of formal verification techniques in industrial settings. Specification patterns represent a promising approach that can fill this gap by enabling nonexpert practitioners to write formal specifications based on reusing solutions to commonly occurring problems. Despite the fact that the specification patterns have been proven suitable for specification of industrial systems, there is no engineer-friendly tool support adequate for industrial adoption. In this paper, we present a tool called SESAMM Specifier in which we integrate a subset of the specification patterns for formal requirements specification, called SPS, into an existing industrial tool-chain. The tool provides the necessary means for the formal specification of system requirements and the later validation of the formally expressed behavior.

引用

页码：167 / 173

页数：7

共 25 条

[1] MODEL-CHECKING IN DENSE REAL-TIME [J].

ALUR, R ;

COURCOUBETIS, C ;

DILL, D .

INFORMATION AND COMPUTATION, 1993, 104 (01) :2-34

[2]

[Anonymous], 1992, TEMPORAL LOGIC REACT, DOI DOI 10.1007/978-1-4612-0931-7

[3]

[Anonymous], 2011, Tech. rep.

[4] Aligning Qualitative, Real-Time, and Probabilistic Property Specification Patterns Using a Structured English Grammar [J].

Autili, Marco ;

Grunske, Lars ;

Lumpe, Markus ;

Pelliccione, Patrizio ;

Tang, Antony .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2015, 41 (07) :620-638

[5] Ten Commandments of formal methods ... Ten years later [J].

Bowen, JP ;

Hinchey, MG .

COMPUTER, 2006, 39 (01) :40-+

[6] AUTOMATIC VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS USING TEMPORAL LOGIC SPECIFICATIONS [J].

CLARKE, EM ;

EMERSON, EA ;

SISTLA, AP .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1986, 8 (02) :244-263

[7]

Cobleigh R. L., 2006, P 14 ACM SIGSOFT INT, P208, DOI [10.1145/1181775.1181801, DOI 10.1145/1181775.1181801]

[8]

Dwyer M. B., 1999, Proceedings of the 1999 International Conference on Software Engineering (IEEE Cat. No.99CB37002), P411, DOI 10.1109/ICSE.1999.841031

[9]

Filipovikj P., 2014, RE 14

[10]

Hassine J., 2008, THESIS

← 1 2 3 →