Formal Specification and Verification of Ubiquitous and Pervasive Systems

被引:27
|
作者
Coronato, Antonio [1 ]
De Pietro, Giuseppe [1 ]
机构
[1] CNR, ICAR, I-00185 Rome, Italy
关键词
Verification; Performance; Formal specification; ubiquitous and pervasive safety-critical applications; methodologies and tools;
D O I
10.1145/1921641.1921650
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
This article presents a methodology to formally express requirements in safety-critical ubiquitous and pervasive applications in order to achieve a higher degree of dependability. In particular, it will be shown how it is possible to formalize and constrict mobility characteristics by combining and extending several formal methods. The article also discusses some issues concerning both static and dynamic verification.
引用
收藏
页数:6
相关论文
共 50 条
  • [21] Formal Specification and Verification of Self-Adaptive Concurrent Systems
    Fakhir, Muhammad Ilyas
    Kazmi, Syed Asad Raza
    [J]. IEEE ACCESS, 2018, 6 : 34790 - 34803
  • [22] Formal Specification and Verification of a Data Replication Approach in Distributed Systems
    Souri, Alireza
    [J]. INTERNATIONAL JOURNAL OF NEXT-GENERATION COMPUTING, 2016, 7 (01): : 18 - 37
  • [23] Automated Formal Verification of the Refined Specification of Digital Systems in HSSL
    Maron, L.
    Macko, D.
    [J]. 2016 INTERNATIONAL CONFERENCE ON EMERGING ELEARNING TECHNOLOGIES AND APPLICATIONS (ICETA), 2016,
  • [24] A formal framework for context-aware systems specification and verification
    Djoudi, Brahim
    Bouanaka, Chafia
    Zeghib, Nadia
    [J]. JOURNAL OF SYSTEMS AND SOFTWARE, 2016, 122 : 445 - 462
  • [25] Specification and formal verification of temporal properties of production automation systems
    Flake, S
    Müller, W
    Pape, U
    Ruf, J
    [J]. INTEGRATION OF SOFTWARE SPECIFICATION TECHNIQUES FOR APPLICATIONS IN ENGINEERING, 2004, 3147 : 206 - 226
  • [26] A Formal Security Framework for Mobile Agent Systems: Specification and Verification
    Loulou, Monia
    Kacem, Ahmed Hadj
    Mosbah, Mohamed
    Jmaiel, Mohamed
    [J]. CRISIS: 2008 THIRD INTERNATIONAL CONFERENCE ON RISKS AND SECURITY OF INTERNET AND SYSTEMS, PROCEEDINGS, 2008, : 69 - 76
  • [27] A formal approach for the specification, verification and control of flexible manufacturing systems
    Zairi, Sajeh
    Zouari, Belhassen
    Pitrac, Laurent
    [J]. ETFA 2007: 12TH IEEE INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION, VOLS 1-3, 2007, : 1031 - +
  • [28] Formal verification of a pervasive messaging system
    Konur, Savas
    Fisher, Michael
    Dobson, Simon
    Knox, Stephen
    [J]. FORMAL ASPECTS OF COMPUTING, 2014, 26 (04) : 677 - 694
  • [29] Formal pervasive verification of a paging mechanism
    Alkassar, Eyad
    Schirmer, Norbert
    Starostin, Artem
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 : 109 - 123
  • [30] Formal Specification of Wireless and Pervasive Healthcare Applications
    Coronato, Antonio
    De Pietro, Giuseppe
    [J]. ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2010, 10 (01)