Practical Formal Verification of Domain-Specific Language Applications

被引：3
|
作者：
Eakman, Greg [1 ]
Reubenstein, Howard [1 ]
Hawkins, Tom [1 ]
Jain, Mitesh [2 ]
Manolios, Panagiotis [2 ]
机构：
[1] BAE Syst, Burlington, MA 01803 USA
[2] Northeastern Univ, Boston, MA 02115 USA
来源：
NASA FORMAL METHODS (NFM 2015) | 2015年 / 9058卷
关键词：
D O I：
10.1007/978-3-319-17524-9_34
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
An application developer's primary task is to produce performant systems that meet their specifications. Formal methods techniques allow engineers to create models and implementations that have a high assurance of satisfying a specification. In this experience report, we take a model-based approach to software development that adds the assurance of formal methods to software construction while automating over 90% of the formal modeling. We discuss a software development methodology and two specific examples that illustrate how to integrate formal methods and their benefits into a traditional (testing-based) software development process.
引用
收藏
页码：443 / 449
页数：7
相关论文
共 50 条
  • [1] A high-level domain-specific language for SIEM (design, development and formal verification)
    Nazir, Anam
    Alam, Masoom
    Malik, Saif U. R.
    Akhunzada, Adnan
    Cheema, Muhammad Nadeem
    Khan, Muhammad Khurram
    Ziang, Yang
    Khan, Tanveer
    Khan, Abid
    [J]. CLUSTER COMPUTING-THE JOURNAL OF NETWORKS SOFTWARE TOOLS AND APPLICATIONS, 2017, 20 (03): : 2423 - 2437
  • [2] A high-level domain-specific language for SIEM (design, development and formal verification)
    Anam Nazir
    Masoom Alam
    Saif U. R. Malik
    Adnan Akhunzada
    Muhammad Nadeem Cheema
    Muhammad Khurram Khan
    Yang Ziang
    Tanveer Khan
    Abid Khan
    [J]. Cluster Computing, 2017, 20 : 2423 - 2437
  • [3] PyFoReL: A Domain-Specific Language for Formal Requirements in Temporal Logic
    Anderson, Jacob
    Hekmatnejad, Mohammad
    Fainekos, Georgios
    [J]. 2022 30TH IEEE INTERNATIONAL REQUIREMENTS ENGINEERING CONFERENCE (RE 2022), 2022, : 266 - 267
  • [4] Photon: A Domain-specific Language for Testing Converged Applications
    Miller, Anne
    Kumar, Balaji
    Singhal, Anukul
    [J]. 2009 IEEE 33RD INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE, VOLS 1 AND 2, 2009, : 942 - 947
  • [5] Towards a Domain-Specific Language to Deploy Applications in the Clouds
    Brandtzaeg, Eirik
    Mohagheghi, Parastoo
    Mosser, Sebastien
    [J]. THIRD INTERNATIONAL CONFERENCE ON CLOUD COMPUTING, GRIDS, AND VIRTUALIZATION (CLOUD COMPUTING 2012), 2012, : 213 - 218
  • [6] A Domain-Specific Language for the Specification of Gesture-based Applications
    Viana, Daniel Leite
    de Medeiros Santos, Andre Luis
    [J]. PROCEEDINGS OF THE 21ST BRAZILIAN SYMPOSIUM ON PROGRAMMING LANGUAGES (SBLP 2017), 2017,
  • [7] Domain-Specific Language for Context-Aware Web Applications
    Nebeling, Michael
    Grossniklaus, Michael
    Leone, Stefania
    Norrie, Moira C.
    [J]. WEB INFORMATION SYSTEM ENGINEERING-WISE 2010, 2010, 6488 : 471 - 479
  • [8] A Domain-Specific Language for Microservices
    Donham, Jacob
    [J]. PROCEEDINGS OF THE 9TH ACM SIGPLAN INTERNATIONAL SYMPOSIUM ON SCALA (SCALA '18), 2018, : 2 - 12
  • [9] A Domain-Specific Language for Defining Static Structure of Database Applications
    Dejanovic, Igor
    Milosavljevic, Gordana
    Perisic, Branko
    Tumbas, Maja
    [J]. COMPUTER SCIENCE AND INFORMATION SYSTEMS, 2010, 7 (03) : 409 - 440
  • [10] ` Domain-Specific Model Verification with QVT
    Elaasar, Maged
    Briand, Lionel
    Labiche, Yvan
    [J]. MODELLING FOUNDATIONS AND APPLICATIONS, 2011, 6698 : 282 - 298
12345