Sciweavers

FM
2009
Springer
189views Formal Methods» more  FM 2009»
13 years 8 months ago
Model-Based GUI Testing Using Uppaal at Novo Nordisk
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...
FM
2009
Springer
154views Formal Methods» more  FM 2009»
13 years 8 months ago
Specification and Verification of Web Applications in Rewriting Logic
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...
María Alpuente, Demis Ballis, Daniel Romero
FM
2009
Springer
153views Formal Methods» more  FM 2009»
13 years 8 months ago
Iterative Refinement of Reverse-Engineered Models by Model-Based Testing
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...
Neil Walkinshaw, John Derrick, Qiang Guo
FM
2009
Springer
146views Formal Methods» more  FM 2009»
13 years 8 months ago
Verifying Real-Time Systems against Scenario-Based Requirements
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...
FM
2009
Springer
134views Formal Methods» more  FM 2009»
13 years 8 months ago
Partial Order Reductions Using Compositional Confluence Detection
Abstract. Explicit state methods have proven useful in verifying safetycritical systems containing concurrent processes that run asynchronously and communicate. Such methods consis...
Frédéric Lang, Radu Mateescu
FM
2009
Springer
169views Formal Methods» more  FM 2009»
14 years 2 months ago
Model Checking Linearizability via Refinement
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...
FM
2009
Springer
95views Formal Methods» more  FM 2009»
14 years 3 months ago
On the Complexity of Synthesizing Relaxed and Graceful Bounded-Time 2-Phase Recovery
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 ...
Borzoo Bonakdarpour, Sandeep S. Kulkarni
FM
2009
Springer
163views Formal Methods» more  FM 2009»
14 years 3 months ago
Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks
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...
FM
2009
Springer
101views Formal Methods» more  FM 2009»
14 years 3 months ago
Formal Reasoning about Expectation Properties for Continuous Random Variables
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&...
FM
2009
Springer
90views Formal Methods» more  FM 2009»
14 years 5 months ago
Fair Model Checking with Process Counter Abstraction
Jun Sun 0001, Yang Liu 0003, Abhik Roychoudhury, S...