Formal Specification and Verification of Ubiquitous and Pervasive Systems

被引：27
|
作者：
Coronato, Antonio [1 ]
De Pietro, Giuseppe [1 ]
机构：
[1] CNR, ICAR, I-00185 Rome, Italy
来源：
ACM TRANSACTIONS ON AUTONOMOUS AND ADAPTIVE SYSTEMS | 2011年 / 6卷 / 01期
关键词：
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 条
  • [31] Formal verification of a ubiquitous hardware component
    Lu, Y
    [J]. EMBEDDED SOFTWARE AND SYSTEMS, 2005, 3605 : 536 - 541
  • [32] Ubiquitous Verification of Ubiquitous Systems
    Wilhelm, Reinhard
    Maffei, Matteo
    [J]. SOFTWARE TECHNOLOGIES FOR EMBEDDED AND UBIQUITOUS SYSTEMS, 2010, 6399 : 47 - 58
  • [33] Formal Specification and Verification of an Extended Security Policy Model for Database Systems
    Hong, Zhu
    Yi, Zhu
    Li Chenyang
    Jie, Shi
    Ge, Fu
    Wang Yuanzhen
    [J]. APTC 2008: THIRD ASIA-PACIFIC TRUSTED INFRASTRUCTURE TECHNOLOGIES CONFERENCE, PROCEEDINGS, 2008, : 132 - 141
  • [34] A formal approach for the specification and verification of trustworthy component-based systems
    Mohammad, Mubarak
    Alagar, Vangalur
    [J]. JOURNAL OF SYSTEMS AND SOFTWARE, 2011, 84 (01) : 77 - 104
  • [35] FORMAL SPECIFICATION AND VERIFICATION OF MULTIMEDIA SYSTEMS IN OPEN DISTRIBUTED-PROCESSING
    BLAIR, L
    BLAIR, G
    BOWMAN, H
    CHETWYND, A
    [J]. COMPUTER STANDARDS & INTERFACES, 1995, 17 (5-6) : 413 - 436
  • [36] Formal specification and verification of reusable communication models for distributed systems architecture
    Rouland, Quentin
    Hamid, Brahim
    Jaskolka, Jason
    [J]. FUTURE GENERATION COMPUTER SYSTEMS-THE INTERNATIONAL JOURNAL OF ESCIENCE, 2020, 108 : 178 - 197
  • [37] Formal specification and verification of a micropayment protocol
    Gouda, MG
    Liu, AX
    [J]. ICCCN 2004: 13TH INTERNATIONAL CONFERENCE ON COMPUTER COMMUNICATIONS AND NETWORKS, PROCEEDINGS, 2004, : 489 - 494
  • [38] Formal Verification of ABAP by Z Specification
    Rodruksa, Soravit
    Pradubsuwun, Denduang
    [J]. PROCEEDINGS OF 2017 14TH INTERNATIONAL JOINT CONFERENCE ON COMPUTER SCIENCE AND SOFTWARE ENGINEERING (JCSSE), 2017,
  • [39] A formal specification and verification of normative multi-agent systems by DisCSP
    Boudhaouia, Aida
    Mazigh, Belhassen
    Missaoui, Ezzine
    [J]. 2017 IEEE/ACS 14TH INTERNATIONAL CONFERENCE ON COMPUTER SYSTEMS AND APPLICATIONS (AICCSA), 2017, : 399 - 406
  • [40] Formal Specification and Verification of Security Guidelines
    Zhioua, Zeineb
    Roudier, Yves
    Ameur, Rabea Boulifa
    [J]. 2017 IEEE 22ND PACIFIC RIM INTERNATIONAL SYMPOSIUM ON DEPENDABLE COMPUTING (PRDC 2017), 2017, : 267 - 273
12345