This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
Abstract. Bounded model checking (BMC) based on satisfiability testing (SAT) has been introduced as a complementary technique to BDDbased symbolic model checking of LTL properties ...
Parking garages that stow and retrieve cars automatically are becoming viable solutions for parking shortages. However, these are complex systems and a number of severe incidents i...
Formal specifications are more useful and easier to develop if they are executable. In this work, we describe a system for executing specifications written in the Java Modeling Lan...
Abstract. We present experiences from a case study where a model-based approach to black-box testing is applied to verify that a Wireless Application Protocol (WAP) gateway conform...
Behrmann et al. posed the question whether "To Store or Not To Store" [1] states during reachability analysis, in order to counter the effects of the well-known state spa...
Abstract. Symbolic state-space generators are notoriously hard to parallelise. However, the Saturation algorithm implemented in the SMART verification tool differs from other seque...
Abstract. Quantitative analysis of quality-of-service metrics is an important tool in early evaluation of service provision. This analysis depends on being able to estimate the ave...
Abstract. In this paper, we concentrate on incremental synthesis of timed automata for automatic addition of different types of bounded response properties. Bounded response