| 1. |
- Abdulla, Parosh Aziz
(författare)
-
Regular model checking
- 2012
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 14:2, s. 109-118
-
Tidskriftsartikel (refereegranskat)
|
|
| 2. |
|
|
| 3. |
- Abdulla, Parosh, et al.
(författare)
-
Regular model checking for LTL(MSO)
- 2012
-
Ingår i: International Journal on Software Tools for Technology Transfer. - Springer : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 14:2, s. 223-241
-
Tidskriftsartikel (refereegranskat)abstract
- Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. We present LTL(MSO), a combination of the logics MSO and LTL as a natural logic for expressing temporal properties to be verified in regular model checking. In other words, LTL(MSO) is a natural specification language for both the system and the property under consideration. LTL(MSO) is a two-dimensional modal logic, where MSO is used for specifying properties of system states and transitions, and LTL is used for specifying temporal properties. In addition, the first-order quantification in MSO can be used to express properties parameterized on a position or process. We give a technique for model checking LTL(MSO), which is adapted from the automata-theoretic approach: a formula is translated to a Buechi regular transition system with a regular set of accepting states, and regular model checking techniques are used to search for models. We have implemented the technique, and show its application to a number of parameterized algorithms from the literature.
|
|
| 4. |
- Artho, Cyrille
(författare)
-
Iterative Delta Debugging
- 2011
-
Ingår i: International Journal on Software Tools for Technology Transfer. - 1433-2779 .- 1433-2787. ; 13:3, s. 223-246
-
Tidskriftsartikel (refereegranskat)
|
|
| 5. |
- Delzanno, Giorgio, et al.
(författare)
-
A lightweight regular model checking approach for parameterized systems
- 2012
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer-Verlag New York. - 1433-2779 .- 1433-2787. ; 14:2, s. 207-222
-
Tidskriftsartikel (refereegranskat)abstract
- In recent years, we have designed a lightweight approach to regular model checking specifically designed for parameterized systems with global conditions. Our approach combines the strength of regular languages, used for representing infinite sets of configurations, with symbolic model checking and approximations. In this paper, we give a uniform presentation of several variations of a symbolic backward reachability scheme in which different classes of regular expressions are used in place of BDDs. The classification of the proposed methods is based on the precision of the resulting approximated analysis.
|
|
| 6. |
- Fantechi, Alessandro, et al.
(författare)
-
Formal methods for railway control systems INTRODUCTION
- 2014
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer. - 1433-2779 .- 1433-2787. ; 16:6, s. 643-646
-
Tidskriftsartikel (refereegranskat)abstract
- The term intelligent transportation systems (ITS) refers to information and communication technology (applied to transport infrastructure and vehicles) that improve transport outcomes such as transport safety, transport productivity, travel reliability, informed travel choices, social equity, environmental performance and network operation resilience. The importance of ITS is increasing as novel driverless/pilotless applications are emerging. This special issue addresses the application of formal methods to model and analyze complex systems in the context of ITS and in particular in the field of railway control systems. In fact, modelling and analysis activities are very important to optimize system life-cycle in the design, development, verification and operational stages, and they are essential whenever assessment and certification is required by international standards. © 2014, Springer-Verlag Berlin Heidelberg.
|
|
| 7. |
|
|
| 8. |
- Lisper, Björn, et al.
(författare)
-
Practical experiences of applying source-level WCET flow analysis to industrial code
- 2013
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 15:1, s. 53-63
-
Tidskriftsartikel (refereegranskat)abstract
- Code-level timing analysis, such as worst-case execution time (WCET) analysis, usually takes place at the binary level. However, many program properties that are important for the analysis, such as constraints on possible program flows, are easier to derive at the source code level since this code contains much more information. Therefore, various source-level analyses can provide valuable support for timing analysis. However, source-level analysis is not always smoothly applicable in industrial settings. In this paper, we report on the experiences of applying source-level analysis to industrial code in the ALL-TIMES project: the promises, the pitfalls, and the workarounds that were developed. We also discuss various approaches to how the difficulties that were encountered can be tackled.
|
|
| 9. |
- Lisper, Björn
(författare)
-
The ALL-TIMES project : Introduction and overview
- 2013
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 15:1, s. 1-8
-
Tidskriftsartikel (refereegranskat)abstract
- Timing analysis is important when designing and verifying time-critical embedded systems. Tool support for timing analysis has existed for a number of years, but the tools have been mostly working in isolation resulting in less efficient timing analysis processes. The European FP7 project ALL-TIMES has addressed this issue by creating interface formats, tool chains, and integrated methodologies for timing analysis where the proper combination of tools and techniques can be used in a given situation. We give an introduction and overview of the ALL-TIMES project: its objectives, tools and partners, work done, and the results.
|
|
| 10. |
- Marrone, Stefano, et al.
(författare)
-
Towards Model-Driven V&V assessment of railway control systems
- 2014
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer. - 1433-2779 .- 1433-2787. ; 16:6, s. 669-683
-
Tidskriftsartikel (refereegranskat)abstract
- Verification and Validation (V&V) activities aiming at certifying railway controllers are among the most critical and time-consuming in system development life cycle. As such, they would greatly benefit from novel approaches enabling both automation and traceability for assessment purposes. While several formal and Model-Based approaches have been proposed in the scientific literature, some of which are successfully employed in industrial settings, we are still far from an integrated and unified methodology which allows guiding design choices, minimizing the chances of failures/non-compliances, and considerably reducing the overall assessment effort. To address these issues, this paper describes a Model-Driven Engineering approach which is very promising to tackle the aforementioned challenges. In fact, the usage of appropriate Unified Modeling Language profiles featuring system analysis and test case specification capabilities, together with tool chains for model transformations and analysis, seems a viable way to allow end-users to concentrate on high-level holistic models and specification of non-functional requirements (i.e., dependability) and support the automation of the V&V process. We show, through a case study belonging to the railway signalling domain, how the approach is effective in supporting activities like system testing and availability evaluation. © 2014, Springer-Verlag Berlin Heidelberg.
|
|
| 11. |
- Merriam, N., et al.
(författare)
-
Estimation of productivity increase for timing analysis tool chains
- 2013
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 15:1, s. 65-84
-
Tidskriftsartikel (refereegranskat)abstract
- Within the scope of the ALL-TIMES project, not only were tool interfaces designed and implemented but also new, powerful timing analysis methodologies constructed. To gauge the effectiveness of these results we used a number of methods to assess the productivity increase that would be achieved by introducing the new techniques. We collect and report on the conclusions of these assessments. © 2012 Springer-Verlag.
|
|
| 12. |
- Wong, Peter Y. H., et al.
(författare)
-
Testing abstract behavioral specifications
- 2014
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer. - 1433-2779 .- 1433-2787. ; 17:1, s. 107-119
-
Tidskriftsartikel (refereegranskat)abstract
- We present a range of testing techniques for the Abstract Behavioral Specification (ABS) language and apply them to an industrial case study. ABS is a formal modeling language for highly variable, concurrent, component-based systems. The nature of these systems makes them susceptible to the introduction of subtle bugs that are hard to detect in the presence of steady adaptation. While static analysis techniques are available for an abstract language such as ABS, testing is still indispensable and complements analytic methods. We focus on fully automated testing techniques including black-box and glass-box test generation as well as runtime assertion checking, which are shown to be effective in an industrial setting.
|
|
