| 1. |
- Behrmann, Gerd, et al.
(författare)
-
Developing UPPAAL over 15 years
- 2011
-
Ingår i: Software, practice & experience. - : Wiley. - 0038-0644 .- 1097-024X. ; 41:2, s. 133-142
-
Tidskriftsartikel (refereegranskat)
|
|
| 2. |
- Berhmann, Gerd, et al.
(författare)
-
Developing UPPAAL over 15 years
- 2011
-
Ingår i: Software - Practice and Experience. - 0038-0644. ; 41:2, s. 133-142
-
Tidskriftsartikel (refereegranskat)abstract
- UPPAAL is a tool suitable for model checking real-time systems described as networks of timed automata communicating by channel synchronizations and extended with integer variables. Its first version was released in 1995 and its development is still very active. It now features an advanced modeling language, a user-friendly graphical interface, and a performant model checker engine. In addition, several flavors of the tool have matured in recent years. In this paper, we present how we managed to maintain the tool during 15 years, its current architecture with its challenges, and we give the future directions of the tool.
|
|
| 3. |
- Berhmann, Gerd, et al.
(författare)
-
UPPAAL 4.0
- 2006
-
Ingår i: Third International Conference on the Quantitative Evaluation of Systems, QEST 2006. - 0769526659 ; , s. 125-126
-
Konferensbidrag (refereegranskat)abstract
- UPPAAL 4.0 is the result of over two and a half years of development and contains many new features, additions to the modeling language, performance improvements, enhancements and polish to the the easy to use graphical user interface, and is accompanied by several open source libraries. The tool and libraries are available free of charge for academic, educational and evaluation purposes from http://www.uppaal.com/. We describe three of the new features: User defined functions, priorities and symmetry reduction.
|
|
| 4. |
- David, Alexandre, et al.
(författare)
-
Model Checking Timed Automata with Priorities using DBM Subtraction
- 2006
-
Ingår i: Lecture Notes in Computer Science, vol 4202. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 9783540450269 ; , s. 128-142
-
Konferensbidrag (refereegranskat)abstract
- In this paper we describe an extension of timed automata with priorities, and efficient algorithms to compute subtraction on DBMs (difference bounded matrices), needed in symbolic model-checking of timed automata with priorities. The subtraction is one of the few operations on DBMs that result in a non-convex set needing sets of DBMs for representation. Our subtraction algorithms are efficient in the sense that the number of generated DBMs is significantly reduced compared to a naive algorithm. The overhead in time is compensated by the gain from reducing the number of resulting DBMs since this number affects the performance of symbolic model-checking. The uses of the DBM subtraction operation extend beyond timed automata with priorities. It is also useful for allowing guards on transitions with urgent actions, deadlock checking, and timed games.
|
|
| 5. |
- David, Alexandre, et al.
(författare)
-
Outils pour le Model-Checking de Systèmes Temporisés
- 2008
-
Ingår i: Approches formelles des systèmes embarqués communicants. - Paris : Hermès science publications. - 9782746219427
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)
|
|
| 6. |
- Hessel, Anders, et al.
(författare)
-
Testing Real-time systems using UPPAAL
- 2008
-
Ingår i: Formal Methods and Testing. - Berlin, Heidelberg : Springer. - 9783540789161 ; , s. 77-117
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- This chapter presents principles and techniques for model-based black-box conformance testing of real-time systems using the Uppaal model-checking tool-suite. The basis for testing is given as a network of concurrent timed automata specified by the test engineer. Relativized input/output conformance serves as the notion of implementation correctness, essentially timed trace inclusion taking environment assumptions into account. Test cases can be generated offline and later executed, or they can be generated and executed online. For both approaches this chapter discusses how to specify test objectives, derive test sequences, apply these to the system under test, and assign a verdict.
|
|
| 7. |
- Jonsson, Bengt, et al.
(författare)
-
On the complexity of equation solving in process algebra
- 1991. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- The problem of designing a system which in a given environment C should satisfy a given specification S can be formulated as "find a system P such that C(P) satisfies the specification S". In process algebra, such problems take the form of equations. We investigate the complexity of solving such equations in process algebra. We consider the problem of deciding whether there is a process P which satisfies an equation of one of the following forms : (the complete form could not be translated) where C is an arbitrary context of some process Algebra, A, B and Q are given processes, S is a modal specification, (˜) is (weak) bisimulation equivalence, is refinement between modal specifications (a generalization of bisimulation equivalence), and | and \L is the parallel and restriction operator of CCS respectively. The main result is that all four problems are PSPACE-hard in the size of the given contexts, processes and specifications. The four problems are still PSPACE-hard if the right-hand side of the equations is required to be deterministic and the number of involved actions is bounded by a small constant. We also give constraints under which the first and third problem can be solved in polynomial time.
|
|
| 8. |
- Larsen, Kim Guldstrand, et al.
(författare)
-
UPPAAL in a nutshell
- 1997
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 1:1-2, s. 134-152
-
Tidskriftsartikel (refereegranskat)
|
|
