Abstract. This paper details a collaboration between Aalborg University and NOVO Nordisk in developing an automatic model-based test generation tool for system testing of the graph...
Ulrik H. Hjort, Jacob Illum Rasmussen, Kim Guldstr...
Abstract. This paper presents a Rewriting Logic framework that formalizes the interactions between Web servers and Web browsers through icating protocol abstracting HTTP. The propo...
Abstract. This paper presents an iterative technique to accurately reverseengineer models of the behaviour of software systems. A key novelty of the approach is the fact that it us...
Abstract. We propose an approach to automatic verification of realtime systems against scenario-based requirements. A real-time system is modeled as a network of Timed Automata (TA...
Kim Guldstrand Larsen, Shuhao Li, Brian Nielsen, S...
Abstract. Explicit state methods have proven useful in verifying safetycritical systems containing concurrent processes that run asynchronously and communicate. Such methods consis...
Abstract. Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires ...
Yang Liu 0003, Wei Chen, Yanhong A. Liu, Jun Sun 0...
The problem of enforcing bounded-time 2-phase recovery in real-time programs is often necessitated by conflict between faulttolerance requirements and timing constraints. In this ...
We study a clock synchronization protocol for the Chess WSN. First, we model the protocol as a network of timed automata and verify various instances using the Uppaal model checker...
Faranak Heidarian, Julien Schmaltz, Frits W. Vaand...
Abstract. Expectation (average) properties of continuous random variables are widely used to judge performance characteristics in engineering and physical sciences. This paper pres...
Osman Hasan, Naeem Abbasi, Behzad Akbarpour, Sofi&...