リアルタイムシステムの形式的手法とその検証ツール [in Japanese] Formal Methods and Verification Tools for Real-Time Systems [in Japanese]
-
- 山根 智 YAMANE Satoshi
- 金沢大学大学院自然科学研究科 Graduate School of Natural Science and Technology, Kanazawa University
Access this Article
Search this Article
Author(s)
-
- 山根 智 YAMANE Satoshi
- 金沢大学大学院自然科学研究科 Graduate School of Natural Science and Technology, Kanazawa University
Abstract
金沢大学理工研究域電子情報学系
Journal
-
- Computer Software
-
Computer Software 25(3), 81-87, 2008-07-25
Japan Society for Software Science and Technology
References: 27
-
1
- <no title>
-
LEWIS H. R.
Finite-State Analysis of Asynchronous Circuits with Bounded Temporal Uncertainty, 1989
Cited by (1)
-
2
- A Logic of Concrete Time Intervals
-
LEWIS H. R.
LICS, 1990, 1990
Cited by (1)
-
3
- <no title>
-
ALUR R.
Model-Checking for Real-Time Systems, 1990
Cited by (1)
-
4
- Symbolic Model Checking for Real-time Systems
-
HENZINGER T. A.
LICS 1992, 394-406, 1992
Cited by (1)
-
5
- Compact Data Structure and State-Space Reduction for Model-Checking Real-Time Systems
-
LARSEN K. G.
J. of Real-Time Systems 25, 255-275, 2003
Cited by (1)
-
6
- Predicate Abstraction for Dense Peal-Time System
-
MOLLER M. O.
ENTCS, 2002
Cited by (1)
-
7
- Timed Automata : Semantics, Algorithms and Tools
-
BENGTSSON J.
LNCS 3098, 87-124, 2003
Cited by (1)
-
8
- <no title>
-
UPPAAL
http://www.uppaal.com/
Cited by (1)
-
9
- チュートリアル : リアルタイムシステムの仕様記述と検証
-
山根智
組込みシンポジウム 2007, 2007
Cited by (1)
-
10
- HyTech : A model checker for hybrid systems
-
HENZINGER T. A.
Soft-ware Tools for Technology Transfer 1, 110-122, 1997
Cited by (1)
-
11
- Timing assumptions and verification of finite-state concurrent systems
-
DILL D.
LNCS 407, 197-212, 1989
Cited by (15)
-
12
- Automata for Modeling Real-Time Systems
-
ALUR R.
Lecture Notes in Computer Science 443, 322-335, 1990
Cited by (17)
-
13
- Decidability of bisimulation equivalences for parallel timer processes
-
CERANS K.
Proc. 4th Int. Workshop on Computer Aided Verification (CAV'92), London, UK, 1992
Cited by (5)
-
14
- The Tool Kronos
-
DAWS C.
LNCS 1066, 208-219, 1996
Cited by (2)
-
15
- Verification of real-time systems by successive over and under approximation
-
DILL D.
LNCS 939, 409-422, 1995
Cited by (4)
-
16
- Approximate reachability analysis of timed automata
-
BALARIN F.
RTSS 1996, 1996
Cited by (1)
-
17
- Symbolic Model-Checking Method Based on Approximations and BDDs for Real-Time Systems
-
YAMANE S.
LNCS 1281, 562-582, 1997
Cited by (1)
-
18
- Data-Structures for the Verification of Timed Automata
-
ASARIN E.
LNCS 1202, 346-360, 1997
Cited by (1)
-
19
- Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems
-
WANG F.
LNCS 1785, 157-171, 2000
Cited by (1)
-
20
- Scaling up Uppaal - Automatic Verification of Real-Time Systems using Compositionality and Abstraction
-
JENSEN H. E.
LNCS 1926, 19-30, 2000
Cited by (1)
-
21
- Uppaal-a tool suite for automatic verification of real-time systems
-
BENGTSSON J.
LNCS 1066, 232-243, 1996
Cited by (8)
-
22
- Formal Verification of Timed Systems : A Survey and Perspective
-
WANG F.
Proceedings of the IEEE 92(8), 2004
Cited by (5)
-
23
- Formal modeling and analysis of an audio/video protocol : an industrial case study using UPPAA
-
HAVELUND K.
IEEE RTSS, 1997, 1997
Cited by (2)
-
24
- An Automata-theoretic Approach to Automatic Program Verification
-
VARDI M. Y.
Proc. LinCS, 1986, 1986
Cited by (4)
-
25
- Deductive Verification of Real-time Systems using STeP
-
BJORNER N.
LNCS 1231, 22-43, 1997
Cited by (4)
-
26
- Times-A tool for modelling and implementation of embedded systems
-
AMNELL T.
LNCS 2280, 460-464, 2002
Cited by (2)
-
27
- PRISM : Probabilistic Symbolic Model Checker
-
KWIATKOWSKA M.
LNCS 2324, 200-204, 2002
Cited by (1)