Generating optimal test cases for real-time systems using DIVINE model checker

2016 ◽  
Author(s):  
Deepak Pal ◽  
Juri Vain
Keyword(s):  
Real Time ◽  
Test Cases ◽  
Real Time Systems ◽  
Model Checker ◽  
Optimal Test ◽  
Time Systems

scholarly journals Time-Optimal Test Cases for Real-Time Systems

2004 ◽  
pp. 234-245 ◽  
Author(s):  
Anders Hessel ◽  
Kim G. Larsen ◽  
Brian Nielsen ◽  
Paul Pettersson ◽  
Arne Skou
Keyword(s):  
Real Time ◽  
Test Cases ◽  
Real Time Systems ◽  
Optimal Test ◽  
Time Optimal ◽  
Time Systems

scholarly journals Online On-the-Fly Testing of Real-time Systems

2003 ◽  
Vol 10 (49) ◽  
Author(s):  
Marius Mikucionis ◽  
Kim G. Larsen ◽  
Brian Nielsen
Keyword(s):  
Real Time ◽  
Test Generation ◽  
Timed Automata ◽  
Online Testing ◽  
Real Time Systems ◽  
Model Checker ◽  
Test Specification ◽  
And Performance ◽  
Automata Network ◽  
Time Systems

In this paper we present a framework, an algorithm and a new tool for online testing of real-time systems based on symbolic techniques used in UPPAAL model checker. We extend UPPAAL timed automata network model to a test specification which is used to generate test primitives and to check the correctness of system responses including the timing aspects. We use timed trace inclusion as a conformance relation between system and specification to draw a test verdict. The test generation and execution algorithm is implemented as an extension to UPPAAL and experiments carried out to examine the correctness and performance of the tool. The experiment results are promising.

Generating test cases for real-time systems from logic specifications

1995 ◽  
Vol 13 (4) ◽  
pp. 365-398 ◽  
Author(s):  
Dino Mandrioli ◽  
Sandro Morasca ◽  
Angelo Morzenti
Keyword(s):  
Real Time ◽  
Test Cases ◽  
Real Time Systems ◽  
Time Systems

scholarly journals Problem Detection in Real-Time Systems by Trace Analysis

2016 ◽  
Vol 2016 ◽  
pp. 1-12 ◽  
Author(s):  
Mathieu Côté ◽  
Michel R. Dagenais
Keyword(s):  
Real Time ◽  
Critical Path ◽  
Test Cases ◽  
Real Time Systems ◽  
Scheduling Problems ◽  
New Approach ◽  
Execution Traces ◽  
Problem Detection ◽  
Execution Model ◽  
Time Systems

This paper focuses on the analysis of execution traces for real-time systems. Kernel tracing can provide useful information, without having to instrument the applications studied. However, the generated traces are often very large. The challenge is to retrieve only relevant data in order to find quickly complex or erratic real-time problems. We propose a new approach to help finding those problems. First, we provide a way to define the execution model of real-time tasks with the optional suggestions of a pattern discovery algorithm. Then, we show the resulting real-time jobs in a Comparison View, to highlight those that are problematic. Once some jobs that present irregularities are selected, different analyses are executed on the corresponding trace segments instead of the whole trace. This allows saving huge amount of time and execute more complex analyses. Our main contribution is to combine the critical path analysis with the scheduling information to detect scheduling problems. The efficiency of the proposed method is demonstrated with two test cases, where problems that were difficult to identify were found in a few minutes.

scholarly journals IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability

2021 ◽  
pp. 552-565
Author(s):  
Étienne André
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Timed Automata ◽  
Robustness Analysis ◽  
Parametric Model ◽  
Timing Constraints ◽  
Real Time Systems ◽  
Model Checker ◽  
Time Systems ◽  
Timed Model Checking

AbstractReal-time systems are notoriously hard to verify due to nondeterminism, concurrency and timing constraints. When timing constants are uncertain (in early the design phase, or due to slight variations of the timing bounds), timed model checking techniques may not be satisfactory. In contrast, parametric timed model checking synthesizes timing values ensuring correctness. takes as input an extension of parametric timed automata (PTAs), a powerful formalism to formally verify critical real-time systems. extends PTAs with multi-rate clocks, global rational-valued variables and a set of additional useful features. We describe here the new features and algorithms offered by  3, that moved along the years from a simple prototype dedicated to robustness analysis to a standalone parametric model checker for timed systems.

scholarly journals Asynchronous testing of real-time systems

10.29007/hcrn ◽  
2018 ◽  
Author(s):  
Puneet Bhateja
Keyword(s):  
Real Time ◽  
Conformance Testing ◽  
Test Case ◽  
Test Cases ◽  
Real Time Systems ◽  
Underlying Theory ◽  
Time Systems ◽  
First In First Out ◽  
Timed Automaton ◽  
Inputs And Outputs

Conformance testing is an operational way of determining whether an implementation conforms to the specification or not. It has a rich underlying theory wherein the specification and the implemen- tation under test (IUT) are each modeled by a timed automaton with inputs and outputs (TAIO), a variant of the classical timed automaton [1]. Test cases generated from the specification TAIO are symbolically executed against the implementation TAIO. Depending upon how test cases interact with the IUT, testing can be synchronous or asynchronous. In synchronous testing a test case interacts with the IUT directly, whereas in asynchronous testing a test case interacts with the IUT through a pair of first-in-first-out (FIFO) channels. Different approaches for synchronous testing of real-time systems have already been proposed [5],[7],[4],[8]. In this paper we propose an approach which is aimed at testing real-time systems asynchronously (i.e., remotely through some medium)

scholarly journals UPPAAL—a Tool Suite for Automatic Verification of Real–Time Systems

1996 ◽  
Vol 3 (58) ◽  
Author(s):  
Johan Bengtsson ◽  
Kim G. Larsen ◽  
Fredrik Larsson ◽  
Paul Pettersson ◽  
Wang Yi
Keyword(s):  
Real Time ◽  
Timed Automata ◽  
Automatic Verification ◽  
Graphical Interface ◽  
Real Time Systems ◽  
Model Checker ◽  
Current Version ◽  
Textual Representations ◽  
Liveness Properties ◽  
Time Systems

Uppaal is a tool suite for automatic verification of safety and<br />bounded liveness properties of real-time systems modeled as networks of<br />timed automata. It includes: a graphical interface that supports graphical<br />and textual representations of networks of timed automata, and automatic<br />transformation from graphical representations to textual format,<br />a compiler that transforms a certain class of linear hybrid systems to<br />networks of timed automata, and a model-checker which is implemented<br />based on constraint-solving techniques. Uppaal also supports diagnostic<br />model-checking providing diagnostic information in case verification of a<br />particular real-time systems fails.<br />The current version of Uppaal is available on the World Wide Web via<br />the Uppaal home page http://www.docs.uu.se/docs/rtmv/uppaal.

Sign in / Sign up

Export Citation Format

Share Document