The PERF Approach for Formal Verification

被引：9

作者：

Benaissa, Nazim ^{[1
]}

Bonvoisin, David ^{[1
]}

Feliachi, Abderrahmane ^{[1
]}

Ordioni, Julien ^{[1
]}

机构：

[1] ING STF QS, RATP, 54 Rue Roger Salengro, F-94724 Fontenay Sous Bois, France

来源：

RELIABILITY, SAFETY, AND SECURITY OF RAILWAY SYSTEMS: MODELLING, ANALYSIS, VERIFICATION, AND CERTIFICATION, RSSRAIL 2016 | 2016年 / 9707卷

关键词：

Formal methods; Verification tool-chain; Railway safety; PERF;

D O I：

10.1007/978-3-319-33951-1_15

中图分类号：

TP39 [计算机的应用];

学科分类号：

081203 ; 0835 ;

摘要：

In order to analyse extensively the safety of the deployed railway software systems, RATP rely on rigorous verification methodologies based on formal methods. During the past few years, RATP has developed a new formal verification method called PERF, supported by a rich proof tool-chain. The main purpose of this method is to perform a non-intrusive verification on the implemented software. Unlike many formal methodologies, it does not require any intervention in the early stages of the software development. In this paper, we present the PERF methodology as well as the different part of its supporting tool-chain with some feedback on the its application in some real projects. We also present the ongoing and future work around the PERF tool-chain.

引用

页码：203 / 214

页数：12

共 50 条

[21] VESAR - A PRAGMATIC APPROACH TO FORMAL SPECIFICATION AND VERIFICATION
ALGAYRES, B
COELHO, V
DOLDI, L
GARAVEL, H
LEJEUNE, Y
RODRIGUEZ, C
[J]. COMPUTER NETWORKS AND ISDN SYSTEMS, 1993, 25 (07): : 779 - 790
[22] Tightly integrate dynamic verification with formal verification: A GSTE based approach
Yang, Jin
Puder, Avi
[J]. ASP-DAC 2005: PROCEEDINGS OF THE ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, VOLS 1 AND 2, 2005, : 327 - 330
[23] A Formal Approach to Safety Verification of Railway Signaling Systems
Russo, Aryldo G., Jr.
Ladenberger, Lukas
[J]. 2012 PROCEEDINGS - ANNUAL RELIABILITY AND MAINTAINABILITY SYMPOSIUM (RAMS), 2012,
[24] A methodology for the formal verification of RISC microprocessors - A functional approach
Merniz, S.
Benmohammed, M.
[J]. 2007 IEEE/ACS INTERNATIONAL CONFERENCE ON COMPUTER SYSTEMS AND APPLICATIONS, VOLS 1 AND 2, 2007, : 492 - +
[25] Formal specification and verification of the SET/A protocol with an integrated approach
Lam, VSW
Padget, J
[J]. CEC 2004: IEEE INTERNATIONAL CONFERENCE ON E-COMMERCE TECHNOLOGY, PROCEEDINGS, 2004, : 229 - 235
[26] Formal verification of a DSP chip using an iterative approach
Habibi, A
Tahar, S
Ghazel, A
[J]. EUROMICRO SYMPOSIUM ON DIGITAL SYSTEM DESIGN, PROCEEDINGS: ARCHITECTURES, METHODS AND TOOLS, 2002, : 12 - 19
[27] A formal approach to modeling and verification of business process collaborations
Corradini, Flavio
Fornari, Fabrizio
Polini, Andrea
Re, Barbara
Tiezzi, Francesco
[J]. SCIENCE OF COMPUTER PROGRAMMING, 2018, 166 : 35 - 70
[28] Techniques for formal verification of digital systems: A system approach
Shojaei, H
Ghayoumi, H
[J]. PROCEEDINGS OF THE EUROMICRO SYSTEMS ON DIGITAL SYSTEM DESIGN, 2004, : 444 - 449
[29] Formal Verification of Pipelined Cryptographic Circuits: A Functional Approach
Bitat, Abir
Merniz, Salah
[J]. INFORMATICA-AN INTERNATIONAL JOURNAL OF COMPUTING AND INFORMATICS, 2021, 45 (04): : 583 - 591
[30] A Formal Methods Approach to Security Requirements Specification and Verification
Rouland, Quentin
Hamid, Brahim
Bodeveix, Jean-Paul
Filali, Mamoun
[J]. 2019 24TH INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2019), 2019, : 236 - 241

← 1 2 3 4 5 →