-
Chapter and Conference Paper
Agent-Based Modelling and Simulation of Decision-Making in Flying Ad-Hoc Networks
At Airbus, an architecture for an ad-hoc network amongst flying platforms, e.g., commercial aircraft, satellites, high altitude platforms, has been developed. Since centralized decision-making for building the...
-
Chapter and Conference Paper
Smart Component Modeling for Complex System Development
This paper presents a proposal for a change in the aircraft development process to cope with the increasing complexity of products and pressure from the market to develop aircraft faster. The key process cha...
-
Chapter and Conference Paper
On Implementable Timed Automata
Generating code from networks of timed automata is a well-researched topic with many proposed approaches, which have in common that they not only generate code for the processes in the network, but necessaril...
-
Chapter and Conference Paper
On Global Scheduling Independency in Networks of Timed Automata
Networks of timed automata are a widely used formalism to model timed systems. Models are often concise and convenient since timed automata abstract from many details of actual implementations. One such abstra...
-
Article
Ready for testing: ensuring conformance to industrial standards through formal verification
The design of distributed, safety-critical real-time systems is challenging due to their high complexity, the potentially large number of components, and complicated requirements and environment assumptions th...
-
Chapter and Conference Paper
The Wireless Fire Alarm System: Ensuring Conformance to Industrial Standards through Formal Verification
The design of distributed, safety critical real-time systems is challenging due to their high complexity, the potentially large number of components, and complicated requirements and environment assumptions. O...
-
Chapter and Conference Paper
Verification of GUI Applications: A Black-Box Approach
In this paper, we propose to base the verification of a GUI application on a reference model used in black-box testing. The reference model is a formal model for the behavior of the GUI application. It is derived...
-
Chapter and Conference Paper
Formal Verification of a Parameterized Data Aggregation Protocol
We report on our experiences on the successful verification of a parameterized wireless fault-tolerant data aggregation protocol. We outline our verification method that involves automatic verification of a mo...
-
Chapter and Conference Paper
Parameterized Verification of Track Topology Aggregation Protocols
We present an approach for the verification aggregation protocols, which may be used to perform critical tasks and thus should be verified. We formalize the class of track topology aggregation protocols and pr...
-
Chapter and Conference Paper
Reducing Quasi-Equal Clocks in Networks of Timed Automata
We introduce the novel notion of quasi-equal clocks and use it to improve the verification time of networks of timed automata. Intuitively, two clocks are quasi-equal if, during each run of the system, they have ...
