共查询到10条相似文献,搜索用时 78 毫秒
1.
2.
KRONOS: a verification tool for real-time systems 总被引:19,自引:1,他引:19
Sergio Yovine 《International Journal on Software Tools for Technology Transfer (STTT)》1997,1(1-2):123-133
3.
Sérgio Vale Aguiar Campos Edmund Clarke 《International Journal on Software Tools for Technology Transfer (STTT)》1999,2(3):260-269
The task of checking if a computer system satisfies its timing specifications is extremely important. These systems are often
used in critical applications where failure to meet a deadline can have serious or even fatal consequences. This paper presents
an efficient method for performing this verification task. In the proposed method a real-time system is modeled by a state-transition
graph represented by binary decision diagrams. Efficient symbolic algorithms exhaustively explore the state space to determine
whether the system satisfies a given specification. In addition, our approach computes quantitative timing information such
as minimum and maximum time delays between given events. These results provide insight into the behavior of the system and
assist in the determination of its temporal correctness. The technique evaluates how well the system works or how seriously
it fails, as opposed to only whether it works or not. Based on these techniques a verification tool called Verus has been constructed. It has been used in the verification of several industrial real-time systems such as the robotics system
described below. This demonstrates that the method proposed is efficient enough to be used in real-world designs. The examples
verified show how the information produced can assist in designing more efficient and reliable real-time systems. 相似文献
4.
5.
6.
Cindy Eisner 《International Journal on Software Tools for Technology Transfer (STTT)》2002,4(1):107-124
We examine the application of symbolic CTL model checking to railway interlocking software. We show that the railway interlocking
systems examined exhibit the characteristics of robustness and locality, and that these characteristics allow optimizations
to the model checking algorithms not possible in the general case. In order to gain a better understanding of robustness and
locality, we examine in detail a small railway interlocking.
Published online: 9 October 2001 相似文献
7.
In this paper we present HySAT, a bounded model checker for linear hybrid systems, incorporating a tight integration of a
DPLL–based pseudo–Boolean SAT solver and a linear programming routine as core engine. In contrast to related tools like MathSAT,
ICS, or CVC, our tool exploits the various optimizations that arise naturally in the bounded model checking context, e.g.isomorphic
replication of learned conflict clauses or tailored decision strategies, and extends them to the hybrid domain. We demonstrate
that those optimizations are crucial to the performance of the tool. 相似文献
8.
In this paper we present efficient symbolic techniques for probabilistic model checking. These have been implemented in PRISM, a tool for the analysis of probabilistic models such as discrete-time Markov chains, continuous-time Markov chains and Markov decision processes using specifications in the probabilistic temporal logics PCTL and CSL. Motivated by the success of model checkers such as SMV which use BDDs (binary decision diagrams), we have developed an implementation of PCTL and CSL model checking based on MTBDDs (multi-terminal BDDs) and BDDs. Existing work in this direction has been hindered by the generally poor performance of MTBDD-based numerical computation, which is often substantially slower than explicit methods using sparse matrices. The focus of this paper is a novel hybrid technique which combines aspects of symbolic and explicit approaches to overcome these performance problems. For typical examples, we achieve a dramatic improvement over the purely symbolic approach. In addition, thanks to the compact model representation using MTBDDs, we can verify systems an order of magnitude larger than with sparse matrices, while almost matching or even beating them for speed. 相似文献
9.
Verification and optimization of a PLC control schedule 总被引:1,自引:0,他引:1
Ed Brinksma Angelika Mader Ansgar Fehnker 《International Journal on Software Tools for Technology Transfer (STTT)》2002,4(1):21-33
We report on the use of model checking techniques for both the verification of a process control program and the derivation
of optimal control schedules. Most of this work has been carried out as part of a case study for the EU VHS project (Verification
of Hybrid Systems), in which the program for a Programmable Logic Controller (PLC) of an experimental chemical plant had to
be designed and verified. The original intention of our approach was to see how much could be achieved here using the standard
model checking environment of SPIN/Promela. As the symbolic calculations of real-time model checkers can be quite expensive
it is interesting to try and exploit the efficiency of established non-real-time model checkers like SPIN in those cases where
promising work-arounds seem to exist. In our case we handled the relevant real-time properties of the PLC controller using
a time-abstraction technique; for the scheduling we implemented in Promela a so-called variable time advance procedure . To
compare and interpret the results we carried out the same case study with the aid of the real-time model checker Uppaal, enhanced
with facilities for cost-guided state space exploration. Both approaches proved sufficiently powerful to verify the design
of the controller and/or derive (time-)optimal schedules within reasonable time and space requirements.
Published online: 2 October 2002
The work reported here was carried out while the second and third authors were employed by the Computer Science Department
of the University of Nijmegen, Netherlands. The second author was supported by an NWO postdoc grant, the third author by an
NWO PhD grant, and both were supported by the EU LTR project VHS (Project No. 26270). 相似文献
10.
Integration – supporting multiple application classes with heterogeneous performance requirements – is an emerging trend
in networks, file systems, and operating systems. We evaluate two architectural alternatives – partitioned and integrated
– for designing next-generation file systems. Whereas a partitioned server employs a separate file system for each application
class, an integrated file server multiplexes its resources among all application classes; we evaluate the performance of the
two architectures with respect to sharing of disk bandwidth among the application classes. We show that although the problem
of sharing disk bandwidth in integrated file systems is conceptually similar to that of sharing network link bandwidth in
integrated services networks, the arguments that demonstrate the superiority of integrated services networks over separate
networks are not applicable to file systems. Furthermore, we show that: an integrated server outperforms the partitioned server
in a large operating region and has slightly worse performance in the remaining region; the capacity of an integrated server
is larger than that of the partitioned server; and an integrated server outperforms the partitioned server by a factor of
up to 6 in the presence of bursty workloads. 相似文献