A toolset for the specification and verification of embedded systems

被引：0
|
作者：
Rebaiaia, ML [1 ]
Benmohamed, M [1 ]
Jaam, JM [1 ]
Hasnah, A [1 ]
机构：
[1] Univ Batna, Dept Comp Sci, Batna, Algeria
来源：
PDPTA'03: PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED PROCESSING TECHNIQUES AND APPLICATIONS, VOLS 1-4 | 2003年
关键词：
UML; verification; real time systems; simulation; rewriting logic; temporal logic;
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Because of many malfunctions of some critical real-time systems (Pentium bug, Ariane lance rocket), which have caused life and billion dollars loss, computer aided formal methods have been developed and successfully applied for the debugging and the verification of hardware/software. The cost of correction of a hardware/software bug is huge enough to justify high expenses to develop more and more verification techniques to safeguard investments. Present software verification technology can certainly be useful but is yet too limited to cope with the formidable challenge caused by the fast development of the technology essentially the embarked one. In this paper, we underline the various features of a tool based on four different systems: a specification, a simulation, a verification and a code-generation models. The ABP protocol is introduced as an application test.
引用
收藏
页码：1539 / 1545
页数：7
相关论文
共 50 条
  • [1] Embedded systems: Challenges in specification and verification
    Pnueli, A
    [J]. EMBEDDED SOFTWARE, PROCEEDINGS, 2002, 2491 : 1 - 14
  • [2] Hidden time model for specification and verification of embedded systems
    Roop, PS
    Sowmya, A
    [J]. 10TH EUROMICRO WORKSHOP ON REAL-TIME SYSTEMS, PROCEEDINGS, 1998, : 98 - 105
  • [3] The TASM toolset: Specification, simulation, and formal verification of real-time systems - (Tool paper)
    Ouimet, Martin
    Lundqvist, Kristina
    [J]. COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2007, 4590 : 126 - +
  • [4] A toolset for modelling and verification of GALS systems
    Ramesh, S
    Sonalkar, S
    D'silva, V
    Chandra, N
    Vijayalakshmi, B
    [J]. COMPUTER AIDED VERIFICATION, 2004, 3114 : 506 - 509
  • [5] Architecture Based Specification and Verification of Embedded Software Systems (Work in Progress)
    Broy, Manfred
    [J]. LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION, PROCEEDINGS, 2008, 17 : 1 - 13
  • [6] Specification and Verification of Distributed Embedded Systems: A Traffic Intersection Product Family
    Olveczky, Peter Csaba
    Meseguer, Jose
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2010, (36): : 137 - 157
  • [7] Architecture Based Specification and Verification of Embedded Software Systems (Work in Progress)
    Broy, Manfred
    [J]. Communications in Computer and Information Science, 2009, 17 : 1 - 13
  • [8] Specification-based verification of embedded systems by automated test case generation
    Kirchsteiger, Christoph M.
    Trummer, Christoph
    Steger, Christian
    Weiss, Reinhold
    Pistauer, Markus
    [J]. DISTRIBUTED EMBEDDED SYSTEMS: DESIGN, MIDDLEWARE AND RESOURCES, 2008, : 35 - +
  • [9] Specification and verification techniques of embedded systems using probabilistic linear hybrid automata
    Mutsuda, Y
    Kato, T
    Yamane, S
    [J]. EMBEDDED SOFTWARE AND SYSTEMS, PROCEEDINGS, 2005, 3820 : 346 - 360
  • [10] SPECIFICATION AND VERIFICATION OF VLSI SYSTEMS
    WILK, A
    PNUELI, A
    [J]. 1989 IEEE INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN: DIGEST OF TECHNICAL PAPERS, 1989, : 460 - 463
12345