ICFEM
2004
Springer
14 years 4 months ago
2004
Springer
Reachability testing is a technique for testing concurrent programs. Reachability testing derives test sequences on-the-fly as the testing process progresses, and can be used to sy...
ICFEM
2004
Springer
14 years 4 months ago
2004
Springer
Abstract. In this paper we present a technique for the Spin tool, inspired by practical experiences with Spin and a FireWire protocol. We show how to guide simulations with Spin, b...
ICFEM
2004
Springer
14 years 4 months ago
2004
Springer
ICFEM
2004
Springer
14 years 4 months ago
2004
Springer
ICFEM
2004
Springer
14 years 4 months ago
2004
Springer
Iterative abstraction refinement has emerged in the last few years as the leading approach to software model checking. In this context Boolean programs are commonly employed as si...
ICFEM
2004
Springer
14 years 4 months ago
2004
Springer
Abstract. We present a correctness proof for a basic file system implementation. This implementation contains key elements of standard Unix file systems such as inodes and fixed...
ICFEM
2004
Springer
14 years 4 months ago
2004
Springer
Abstract. The integrated logic-based modeling language, Timed Communicating Object Z (TCOZ), is well suited for presenting complete and coherent requirement models for complex real...
ICFEM
2004
Springer
14 years 4 months ago
2004
Springer
Abstract. We present a practical approach to a formal analysis of UMLbased models. This is achieved by an underlying formal representation in Z, which allows us to pose and dischar...
ICFEM
2004
Springer
14 years 4 months ago
2004
Springer
ICFEM
2004
Springer
14 years 4 months ago
2004
Springer
