| 1. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
The KeY platform for verification and analysis of java programs
- 2014
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 8471:8471, s. 55-71
-
Konferensbidrag (refereegranskat)abstract
- The KeY system offers a platform of software analysis tools for sequential Java. Foremost, this includes full functional verification against contracts written in the Java Modeling Language. But the approach is general enough to provide a basis for other methods and purposes: (i) complementary validation techniques to formal verification such as testing and debugging, (ii) methods that reduce the complexity of verification such as modularization and abstract interpretation, (iii) analyses of non-functional properties such as information flowsecurity, and (iv) sound program transformation and code generation. We show that deductive technology that has been developed for full functional verification can be used as a basis and framework for other purposes than pure functional verification. We use the current release of the KeY system as an example to explain and prove this claim.
|
|
| 2. |
- Sidorenko, Galina, 1985-, et al.
(författare)
-
The CAR Approach : Creative Applied Research Experiences for Master’s Students in Autonomous Platooning
- 2021
-
Ingår i: 2021 30th IEEE International Conference on Robot and Human Interactive Communication, RO-MAN 2021. - : IEEE. - 9781665404921 - 9781665446372 ; , s. 214-221
-
Konferensbidrag (refereegranskat)abstract
- Autonomous vehicles (AVs) are crucial robotic systems that promise to improve our lives via safe, efficient, and inclusive transport-while posing some new challenges for the education of future researchers in the area, that our current research and education might not be ready to deal with: In particular, we don't know what the AVs of the future will look like, practical learning is restricted due to cost and safety concerns, and a high degree of multidisciplinary knowledge is required. Here, following the broad outline of Active Student Participation theory, we propose a pedagogical approach targeted toward AVs called CAR that combines Creativity theory, Applied demo-oriented learning, and Real world research context. Furthermore, we report on applying the approach to stimulate learning and engagement in a master's course, in which students freely created a demo with 10 small robots running ROS2 and Ubuntu on Raspberry Pis, in connection to an ongoing research project and a real current problem (SafeSmart and COVID-19). The results suggested the feasibility of the CAR approach for enabling learning, as well as mutual benefits for both the students and researchers involved, and indicated some possibilities for future improvement, toward more effective integration of research experiences into second cycle courses. © 2021 IEEE.
|
|
| 3. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
Real-time java API specifications for high coverage test generation
- 2012
-
Ingår i: 10th International Workshop on Java Technologies for Real-Time and Embedded Systems (JTRES 2012), Copenhagen, 24 - 26 October 2012. - New York, NY, USA : ACM. - 9781450316880 ; , s. 145-154
-
Konferensbidrag (refereegranskat)abstract
- We present the test case generation method and tool KeYTestGen in the context of real-time Java applications and libraries. The generated tests feature strong coverage criteria, like the Modified Condition/Decision Criterion, by construction. This is achieved by basing the test generation on formal verification techniques, namely the KeY system for Java source code verification. Moreover, we present formal specifications for the classes and methods in the real-time Java API. These specifications are used for symbolic execution when generating tests for real-time Java applications, and for oracle construction when generating tests for real-time Java library implementations. The latter application exhibited a mismatch between a commercial library implementation and the official RTSJ documentation. Even if there is a rationale behind this particular inconsistency, it demonstrates the effectiveness of our method on productioncode.
|
|
| 4. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
The KeY System: Integrating Object-Oriented Design and Formal Methods
- 2002
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783540433538 ; 2306, s. 327-330
-
Konferensbidrag (refereegranskat)abstract
- This paper gives a brief description of the KeY system, a tool written as part of the ongoing KeY project1, which is aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verification. The KeY system consists of a commercial CASE tool enhanced with functionality for formal specification and deductive verification.
|
|
| 5. |
- Aichernig, Bernhard K., et al.
(författare)
-
Model Learning and Model-Based Testing
- 2018
-
Ingår i: Machine Learning for Dynamic Software Analysis. - Heidelberg : Springer. - 9783319965611 - 9783319965628 ; , s. 74-100
-
Konferensbidrag (refereegranskat)abstract
- We present a survey of the recent research efforts in integrating model learning with model-based testing. We distinguished two strands of work in this domain, namely test-based learning (also called test-based modeling) and learning-based testing. We classify the results in terms of their underlying models, their test purpose and techniques, and their target domains. © Springer International Publishing AG
|
|
| 6. |
- Aramrattana, Maytheewat, 1988-, et al.
(författare)
-
Team Halmstad Approach to Cooperative Driving in the Grand Cooperative Driving Challenge 2016
- 2018
-
Ingår i: IEEE transactions on intelligent transportation systems (Print). - Piscataway, N.J. : Institute of Electrical and Electronics Engineers Inc.. - 1524-9050 .- 1558-0016. ; 19:4, s. 1248-1261
-
Tidskriftsartikel (refereegranskat)abstract
- This paper is an experience report of team Halmstad from the participation in a competition organised by the i-GAME project, the Grand Cooperative Driving Challenge 2016. The competition was held in Helmond, The Netherlands, during the last weekend of May 2016. We give an overview of our car’s control and communication system that was developed for the competition following the requirements and specifications of the i-GAME project. In particular, we describe our implementation of cooperative adaptive cruise control, our solution to the communication and logging requirements, as well as the high level decision making support. For the actual competition we did not manage to completely reach all of the goals set out by the organizers as well as ourselves. However, this did not prevent us from outperforming the competition. Moreover, the competition allowed us to collect data for further evaluation of our solutions to cooperative driving. Thus, we discuss what we believe were the strong points of our system, and discuss post-competition evaluation of the developments that were not fully integrated into our system during competition time. © 2000-2011 IEEE.
|
|
| 7. |
- Beckert, Bernhard, et al.
(författare)
-
A Program Logic for Handling Java Card's Transaction Mechanism
- 2003
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 3540008993 ; 2621, s. 246-260
-
Konferensbidrag (refereegranskat)abstract
- In this paper we extend a program logic for verifying Java Card applications by introducing a "throughout" operator that allows us to prove "strong" invariants. Strong invariants can be used to ensure "rip out" properties of Java Card programs (properties that are to be maintained in case of unexpected termination of the program). Along with introducing the "throughout" operator, we show how to handle the Java Card transaction mechanism (and, thus, conditional assignments) in our logic. We present sequent calculus rules for the extended logic.
|
|
| 8. |
- David, Jennifer, 1987-, et al.
(författare)
-
Design and Development of a Hexacopter for the Search and Rescue of a Lost Drone
- 2019
-
Konferensbidrag (refereegranskat)abstract
- Search and rescue with an autonomous robot is an attractive and challenging task within the research community. This paper presents the development of an autonomous hexacopter that is designed for retrieving a lost object, like a drone, from a vast-open space, like a desert area. Navigating its path with a proposed coverage path planning strategy, the hexacopter can efficiently search for a lost target and locate it using an image-based object detection algorithm. Moreover, after the target is located, our hexacopter can grasp it with a customised gripper and transport it back to a destined location. It is also capable of avoiding static obstacles and dynamic objects. The proposed system was realised in simulations before implementing it in a real hardware setup, i.e. assembly of the drone, crafting of the gripper, software implementation and testing under real-world scenarios. The designed hexacopter won the best UAV design award at the CPS-VO 2018 Competition held in Arizona, USA.
|
|
| 9. |
- Entekhabi, Sina, 1989-, et al.
(författare)
-
Automated and Efficient Test-Generation for Grid-Based Multiagent Systems : Comparing Random Input Filtering versus Constraint Solving
- 2023
-
Ingår i: ACM Transactions on Software Engineering and Methodology. - New York, NY : Association for Computing Machinery (ACM). - 1049-331X .- 1557-7392. ; 33:1
-
Tidskriftsartikel (refereegranskat)abstract
- Automatic generation of random test inputs is an approach that can alleviate the challenges of manual test case design. However, random test cases may be ineffective in fault detection and increase testing cost, especially in systems where test execution is resource- and time-consuming. To remedy this, the domain knowledge of test engineers can be exploited to select potentially effective test cases. To this end, test selection constraints suggested by domain experts can be utilized either for filtering randomly generated test inputs or for direct generation of inputs using constraint solvers. In this article, we propose a domain specific language (DSL) for formalizing locality-based test selection constraints of autonomous agents and discuss the impact of test selection filters, specified in our DSL, on randomly generated test cases. We study and compare the performance of filtering and constraint solving approaches in generating selective test cases for different test scenario parameters and discuss the role of these parameters in test generation performance. Through our study, we provide criteria for suitability of the random data filtering approach versus the constraint solving one under the varying size and complexity of our testing problem. We formulate the corresponding research questions and answer them by designing and conducting experiments using QuickCheck for random test data generation with filtering and Z3 for constraint solving. Our observations and statistical analysis indicate that applying filters can significantly improve test efficiency of randomly generated test cases. Furthermore, we observe that test scenario parameters affect the performance of the filtering and constraint solving approaches differently. In particular, our results indicate that the two approaches have complementary strengths: random generation and filteringworks best for large agent numbers and long paths, while its performance degrades in the larger grid sizes and more strict constraints. On the contrary, constraint solving has a robust performance for large grid sizes and strict constraints, while its performance degrades with more agents and long paths. © 2023 Copyright held by the owner/author(s).
|
|
| 10. |
- Entekhabi, Sina, 1989-, et al.
(författare)
-
Domain Specific Language for Testing Grid-based Multiagent Autonomous Systems
-
Annan publikation (övrigt vetenskapligt/konstnärligt)abstract
- The automatic generation of random test inputs offers a potential solution to the challenges associated with manual test case design. However, the use of random test cases may prove ineffective for fault detection and can escalate testing costs, particularly in systems where test execution demands significant resources and time. To address this issue, leveraging the domain knowledge of test engineers becomes crucial for selecting test cases with the potential for effectiveness. One approach involves utilizing test selection constraints recommended by domain experts, which can be applied to generate targeted test inputs. In our previous paper, we introduced a domain-specific language (DSL) designed to formalize locality-based test selection constraints specifically tailored for autonomous agents. In this work, we devise an extended DSL for specifying more detailed test scenarios for a more elaborate model of autonomous agents and environment. We design a questionnaire and ask several experts' opinions about the usefulness of the DSL and also design an experiment to compare the efficiency, in terms of time needed to reach a failure, of the extended DSL with the initially proposed one. The questionnaire results show that some features of the extended DSL look useful in the experts' opinion, and the experiment results show that testing with the extended DSL can considerably improve the efficiency of the testing process.
|
|
| 11. |
- Entekhabi, Sina, et al.
(författare)
-
Locality-Based Test Selection for Autonomous Agents
- 2022
-
Ingår i: Testing Software and Systems. - Cham : Springer Science+Business Media B.V.. - 9783031046728 ; , s. 73-89
-
Konferensbidrag (refereegranskat)abstract
- Automated random testing is useful in finding faulty corner cases that are difficult to find by using manually-defined fixed test suites. However, random test inputs can be inefficient in finding faults, particularly in systems where test execution is time- and resource-consuming. Hence, filtering out less-effective test cases by applying domain knowledge constraints can contribute to test effectiveness and efficiency. In this paper, we provide a domain specific language (DSL) for formalising locality-based test selection constraints for autonomous agents. We use this DSL for filtering randomly generated test inputs. To evaluate our approach, we use a simple case study of autonomous agents and evaluate our approach using the QuickCheck tool. The results of our experiments show that using domain knowledge and applying test selection filters significantly reduce the required number of potentially expensive test executions to discover still existing faults. We have also identified the need for applying filters earlier during the test data generation. This observation shows the need to make a more formal connection between the data generation and the DSL-based filtering, which will be addressed in future work. © 2022, IFIP International Federation for Information Processing.
|
|
| 12. |
- Entekhabi, Sina, 1989-
(författare)
-
Test Automation for Grid-Based Multiagent Autonomous Systems
- 2024
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Traditional software testing usually comes with manual definitions of test cases. This manual process can be time-consuming, tedious, and incomplete in covering important but elusive corner cases that are hardly identifiable. Automatic generation of random test cases emerges as a strategy to mitigate the challenges associated with the manual test case design. However, the effectiveness of random test cases in fault detection may be limited, leading to increased testing costs, particularly in systems where test execution demands substantial resources and time. Leveraging the domain knowledge of test experts can guide the automatic random generation of test cases to more effective zones. In this thesis, we target quality assurance of multiagent autonomous systems and aim to automate test generation for them by applying the domain knowledge of test experts.To formalize the specification of the domain expert's knowledge, we introduce a small Domain Specific Language (DSL) for formal specification of particular locality-based constraints for grid-based multiagent systems. We initially employ this DSL for filtering randomly generated test inputs. Then, we evaluate the effectiveness of the generated test cases through an experiment on a case study of autonomous agents. Applying statistical analysis on the experiment results demonstrates that utilizing the domain knowledge to specify test selection criteria for filtering randomly generated test cases significantly reduces the number of potentially costly test executions to identify the persisting faults. Domain knowledge of experts can also be utilized to directly generate test inputs with constraint solvers. We conduct a comprehensive study to compare the performance of filtering random cases and constraint-solving approaches in generating selective test cases across various test scenario parameters. The examination of these parameters provides criteria for determining the suitability of random data filtering versus constraint solving, considering the varying size and complexity of the test input generation constraint. To conduct our experiments, we use QuickCheck tool for random test data generation with filtering, and we employ Z3 for constraint solving. The findings, supported by observations and statistical analysis, reveal that test scenario parameters impact the performance of filtering and constraint-solving approaches differently. Specifically, the results indicate complementary strengths between the two approaches: random generation and filtering approach excels for the systems with a large number of agents and long agent paths but shows degradation in larger grid sizes and stricter constraints. Conversely, constraint solving approach demonstrates robust performance for large grid sizes and strict constraints but experiences degradation with increased agent numbers and longer paths.Our initially proposed DSL is limited in its features and is only capable of specifying particular locality-based constraints. To be able to specify more elaborate test scenarios, we extend that DSL based on a more intricate model of autonomous agents and their environment. Using the extended DSL, we can specify test oracles and test scenarios for a dynamic grid environment and agents having several attributes. To assess the extended DSL's utility, we design a questionnaire to gather opinions from several experts and also run an experiment to compare the efficiency of the extended DSL with the initially proposed one. The questionnaire results indicate that the extended DSL was successful in specifying several scenarios that the experts found more useful than the scenarios specified by the initial DSL. Moreover, the experimental results demonstrate that testing with the extended DSL can significantly reduce the number of test executions to detect system faults, leading to a more efficient testing process.
|
|
| 13. |
- Ernst, Gidon, et al.
(författare)
-
VerifyThis – Verification Competition with a Human Factor
- 2019
-
Ingår i: Lecture Notes in Computer Science. - Heidelberg : Springer. - 0302-9743 .- 1611-3349. - 9783030175016 - 9783030175023 ; 11429, s. 176-195
-
Tidskriftsartikel (refereegranskat)abstract
- VerifyThis is a series of competitions that aims to evaluatethe current state of deductive tools to prove functional correctness of programs. Such proofs typically require human creativity, and hence iti s not possible to measure the performance of tools independently of the skills of its user. Similarly, solutions can be judged by humans only. Inthis paper, we discuss the role of the human in the competition setup and explore possible future changes to the current format. Regarding the impact of VerifyThis on deductive verification research, a survey conducted among the previous participants shows that the event is a key enabler for gaining insight into other approaches, and that it fosters collaboration and exchange. © 2019, The Author(s).
|
|
| 14. |
- Grahl, Daniel, et al.
(författare)
-
Modular Specification and Verification
- 2016
-
Ingår i: Deductive Software Verification – The KeY Book. - Heidelberg : Springer. - 9783319498119 - 9783319498126 ; , s. 289-351
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- In this chapter, concepts already addressed in previous chapters are reconsidered and extended to cater for modularity. In particular, it is shown how method contracts can be used in proofs (as opposed to being verified themselves). Another central topic is nonfunctional framing information, i.e., information on what locations a method may write to or read from. But, there are also items that are discussed here in depth for the first time: model methods, an abstraction of Java methods that are only used in specification, verification of recursive methods, and object invariants. For any of the arising proof obligations the calculus rules needed to dispatch them are shown. © Springer International Publishing AG 2016.
|
|
| 15. |
- Huisman, Marieke, et al.
(författare)
-
VerifyThis 2017 : A Program Verification Competition
- 2017
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- VerifyThis 2017 was a two-day program verification competition which took place from April 22-23rd, 2017 in Uppsala, Sweden as part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2017). It was the sixth instalment in the VerifyThis competition series. This article provides an overview of the VerifyThis 2017 event, the challenges that were posed during the competition, and a high-level overview of the solutions to these challenges. It concludes with the results of the competition.
|
|
| 16. |
- Hähnle, Reiner, 1962, et al.
(författare)
-
The KeY Tool
- 2005
-
Ingår i: Software and Systems Modeling. - 1619-1374 .- 1619-1366. ; 4:1, s. 32-54
-
Tidskriftsartikel (refereegranskat)
|
|
| 17. |
- Hähnle, Reiner, 1962, et al.
(författare)
-
Verification of Safety Properties in the Presence of Transactions
- 2005
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. ; 3362, s. 151-171
-
Tidskriftsartikel (refereegranskat)abstract
- The JavaCard transaction mechanism can ensure that a sequence of statements either is executed to completion or is not executed at all. Transactions make verification of JavaCard programs considerably more difficult, because they cannot be formalised in a logic based on pre- and postconditions. The KeY system includes an interactive theorem prover for JavaCard source code that models the full JavaCard standard including transactions. Based on a case study of realistic size we show the practical difficulties encountered during verification of safety properties. We provide an assessment of current JavaCard source code verification, and we make concrete suggestions towards overcoming the difficulties by design for verification. The main conclusion is that largely automatic verification of realistic JavaCard software is possible provided that it is designed with verification in mind from the start.
|
|
| 18. |
- Kunze, Sebastian, 1990-, et al.
(författare)
-
Generation of Failure Models through Automata Learning
- 2016
-
Ingår i: Proceedings. - Los Alamitos : IEEE Computer Society. - 9781509025718 ; , s. 22-25
-
Konferensbidrag (refereegranskat)abstract
- In the context of the AUTO-CAAS project that deals with model-based testing techniques applied in the automotive domain, we present the preliminary ideas and results of building generalised failure models for non-conformant software components. These models are a necessary building block for our upcoming efforts to detect and analyse failure causes in automotive software built with AUTOSAR components. Concretely, we discuss how to build these generalised failure models using automata learning techniques applied to a guided model-based testing procedure of a failing component. We illustrate our preliminary findings and experiments on a simple integer queue implemented in the C programming language. © 2016 IEEE.
|
|
| 19. |
- Mostowski, Wojciech, 1976-, et al.
(författare)
-
Dynamic Dispatch for Method Contracts Through Abstract Predicates
- 2016
-
Ingår i: Lecture Notes in Computer Science. - Cham : Springer. - 0302-9743 .- 1611-3349. ; 9800, s. 238-267
-
Tidskriftsartikel (refereegranskat)abstract
- Dynamic method dispatch is a core feature of object-oriented programming by which the executed implementation for a polymorphic method is only chosen at runtime. In this paper, we present a specification and verification methodology which extends the concept of dynamic dispatch to design-by-contract specifications.The formal specification language JML has only rudimentary means for polymorphic abstraction in expressions. We promote these to fully flexible specification-only query methods called model methods that can, like ordinary methods, be overridden to give specifications a new semantics in subclasses in a transparent and modular fashion. Moreover, we allow them to refer to more than one program state which give us the possibility to fully abstract and encapsulate two-state specification contexts, i.e., history constraints and method postconditions. Finally, we provide an elegant and flexible mechanism to specify restrictions on specifications in subtypes. Thus behavioural subtyping can be enforced, yet it still allows for other specification paradigms.We provide the semantics for model methods by giving a translation into a first order logic and according proof obligations. We fully implemented this framework in the KeY program verifier and successfully verified relevant examples. We have also implemented an extension to KeY to support permission-based verification of concurrent Java programs. In this context model methods provide a modular specification method to treat code synchronisation through API methods. © The Author(s) 2016.
|
|
| 20. |
- Mostowski, Wojciech, 1976-
(författare)
-
Dynamic Frames Based Verification Method for Concurrent Java Programs
- 2016
-
Ingår i: Verified Software. - New York : Springer International Publishing Switzerland. - 9783319296128 - 9783319296135 ; , s. 124-141
-
Konferensbidrag (refereegranskat)abstract
- In this paper we discuss a verification method for concurrent Java programs based on the concept of dynamic frames. We build on our earlier work that proposes a new, symbolic permission system for concurrent reasoning and we provide the following new contributions. First, we describe our approach for proving program specifications to be self-framed w.r.t. permissions, which is a necessary condition to maintain soundness in concurrent reasoning. Second, we show how we use predicates to provide modular and reusable specifications for program synchronisation points, like locks or forked threads. Our work primarily targets the KeY verification system with its specification language JML* and symbolic execution proving method. Hence, we also give the current status of the work on implementation and we discuss some examples that are verifiable with KeY. © Springer International Publishing Switzerland 2016
|
|
| 21. |
- Mostowski, Wojciech, 1976
(författare)
-
Formal Development of Safe and Secure Java Card Applets
- 2005
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- This thesis is concerned with formal development of Java Card applets. Java Card is a technology that provides a means to program smart cards with (a subset of) the Java language. In recent years Java Card technology gained great interest in the formal verification community. There are two reasons for this. Due to the sensitive nature (e.g., security, maintenance costs) of Java Card applets, formal verification for Java Card is highly desired. Moreover, because of the relative simplicity of the programming language, Java Card is also a feasible target for formal verification. The formal verification platform that we used in our research is the KeY system developed in the KeY Project. One of the main objectives of our research is to find out how far formal verification for industrial size Java Card applets goes, in terms of usability, automation, and power (expressivity of constraints). Furthermore, we investigated practical and theoretical shortcomings of the verification techniques and development methods for Java Card applets. As a result, we adapted a program logic for Java Card to be able to express interesting, meaningful safety and security properties (strong invariants) and proposed design guidelines to support and ease formal verification (design for verification). We performed extensive practical experiments with the KeY system to justify and evaluate our work. Formal aspects of our research concentrate on source code level verification of Java Card programs with interactive and automated theorem proving. Our work has been driven by certain assumptions, motivated by the KeY Project's philosophy: (1) formal verification should be accessible to software engineers without years of training in formal methods, (2) we should be able to perform full verification whenever needed, i.e., we want to handle complex Java Card applets that involve Java Card specific features, like atomic transactions and object persistency, (3) the verified code should not be subjected to translations, simplifications, intermediate representations, etc., and finally, (4) the properties that we prove should relate to important safety and security issues in Java Card development. We relate to these goals in our work.
|
|
| 22. |
- Mostowski, Wojciech, 1976
(författare)
-
Formalisation and Verification of Java Card Security Properties in Dynamic Logic
- 2004
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We present how common Java Card security properties can be formalised in Dynamic Logic and verified, mostly automatically, with the KeY system. The properties we consider, are a large subset of properties that are ofimportance to the smart card industry. We discuss the properties one by one, illustrate them withexamples of real-life, industrial size, Java Card applications, and show how the properties are verified with the KeY Prover - an interactive theorem prover for Java Card source code based on a version of Dynamic Logicthat models the full Java Card standard. We report on the experience related to formal verification of Java Card programs we gained during the course of this work. Thereafter, we present the current state of the art offormal verification techniques offered by the KeY system and give an assessment of interactive theorem proving as an alternative to static analysis.
|
|
| 23. |
- Mostowski, Wojciech, 1976-
(författare)
-
From Explicit to Implicit Dynamic Frames in Concurrent Reasoning for Java
- 2020
-
Ingår i: Deductive Software Verification. - Heidelberg : Springer. ; , s. 177-203
-
Bokkapitel (refereegranskat)abstract
- In our earlier work we presented a method for formal verification of concurrent Java programs based on Dynamic Logic and symbolic permissions. Embedded within the explicit dynamic frames method realised through JML⁎ specifications, permissions to heap locations and the actual heap location values are tracked separately and require two independent and often overlapping frame specifications. This is in contrast to well established Separation Logic and sibling frameworks, where program frames are inferred from permission annotations that already provide implicit framing information.In this paper we show how to avoid redundant frame specifications and move towards the implicit framing approach in our method. We strive to keep as much as possible of the existing reasoning framework to preserve the general verification philosophy and implementation of our verification tool, the KeY verifier. We achieve our goal by only a small alteration of the existing proof obligation generation without changing any core part of the underlying logic, in particular, we maintain its closed character. However, even though specifications become more natural and less redundant, the indirect character of the specifications introduces a clear performance penalty for the verification engine.We then proceed to a brief discussion why, under our minimal approach assumptions, this extension is still not sufficient to translate Separation Logic specifications into our framework. © 2020, Springer Nature Switzerland AG.
|
|
| 24. |
- Mostowski, Wojciech, 1976-
(författare)
-
Implications of Deductive Verification on Research Quality : Field Study
- 2022
-
Ingår i: The Logic of Software. A Tasting Menu of Formal Methods. - Cham : Springer. - 9783031081651 - 9783031081668 ; , s. 370-381
-
Bokkapitel (refereegranskat)abstract
- This short paper discusses a handful of perhaps obvious, but important observations about KeY, the state-of-the-art deductive verification tool for Java programs. Two light research ideas surface out during the admittedly divergent discussion, both of which seem to be little explored, at least in the given context. Not all projects survive for as long as KeY does, it takes a good idea and dedicated people for that to happen. Hence, the paper also contributes with a formally proved correspondence between using KeY and being a good researcher. Apart from that, considering the occasion to which this paper is dedicated, a handful of memories about Prof. Hähnle are also shared. © 2022, Springer Nature Switzerland AG.
|
|
| 25. |
- Mostowski, Wojciech, 1976-
(författare)
-
Model-based fault injection for testing gray-box systems
- 2019
-
Ingår i: The Journal of logical and algebraic methods in programming. - Amsterdam : Elsevier. - 2352-2208 .- 2352-2216. ; 103, s. 31-45
-
Tidskriftsartikel (refereegranskat)abstract
- Motivated by applications in the automotive domain, particularly the Autosar basic software standard, we present a technique to improve model-based testing by allowing model-level fault injections. These models are plugged into a larger system as executable components to test it for general tolerance to slightly varying, possibly faulty components or library implementations. Such model execution is possible through applying an automated mocking mechanism and model cross-referencing. Systematic modelling and testing is possible by having comprehensive fault models which both simulate faults and guide the model-based testing procedure towards quicker discovery of these faults. We show the principles of our method on an illustrative example and discuss how it is implemented in a commercial model-based testing tool QuickCheck and applied to a more realistic case study. More generally, this work explores multi-purpose (or meta) modelling – an approach where one parametric model is used for different test targets, like functional testing or safety testing.
|
|
| 26. |
- Mostowski, Wojciech, 1976-, et al.
(författare)
-
Modelling of Autosar Libraries for Large Scale Testing
- 2017
-
Ingår i: 2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017). ; 244, s. 184-199
-
Konferensbidrag (refereegranskat)abstract
- We demonstrate a specific method and technology for model-based testing of large software projects with the QuickCheck tool using property-based specifications. Our specifications are very precise, state-full models of the software under test (SUT). In our approach we define (a) formal descriptions of valid function call sequences (public API), (b) postconditions that check the validity of each call, and (c) call-out specifications that define and validate external system interactions (SUT calling external API). The QuickCheck tool automatically generates and executes tests from these specifications. Commercially, this method and tool have been used to test large parts of the industrially developed automotive libraries based on the Autosar standard. In this paper, we exemplify our approach with a circular buffer specified by Autosar, to demonstrate the capabilities of the model-based testing method of QuickCheck. Our example is small compared to the commercial QuickCheck models, but faithfully addresses many of the same challenges. © W. Mostowski, T. Arts, J. Hughes.
|
|
| 27. |
- Mostowski, Wojciech, 1976
(författare)
-
Rigorous Development of Java Card Applications
- 2002
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract
- We present an approach to rigorous, tool supported design and development of Java Card applications. We employ the Unified Modelling Language (UML) and formal methods for object oriented software development in our approach. Our goal is to make Java Card applications robust "by design", to make the development process independent of the Java Card platform used and to enable applications to be verified by the KeY system. First we analyse the current situation of Java Card application development, then we present a reallife Java Card case study and describe the problems we found that should be addressed by rigorous development. Finally we propose some solutions to selected problems by using UML specifications, software design patterns, formal specifications and a modern CASE tool support.
|
|
| 28. |
- Mostowski, Wojciech, 1976, et al.
(författare)
-
Specifying Java Card API in OCL
- 2004
-
Ingår i: OCL 2.0 Workshop at UML 2003 Conference. ; 102:C, s. 3-19
-
Konferensbidrag (refereegranskat)abstract
- We discuss the development of an OCL specification for theJava Card API. The main purpose of this specification is tosupport and aid the verification of Java Card programs in the KeY system. The main goal of the KeY system is tointegrate object oriented design and formal methods. The already existing specification written in JML (Java Modelling Language) has been used as a starting point for the development of the OCL specification. In this paper we report on the problems that we encountered when writing the specification and their solutions, we present the most interesting parts of the specification, we report on successful verification attempts and finally we evaluate OCL and compare it to JML in the context of Java Card program specification and verification.
|
|
| 29. |
- Mostowski, Wojciech, 1976
(författare)
-
Towards Development of Safe and Secure Java Card Applets
- 2002
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- This thesis is concerned with different aspects of Java Card application development and use of formal methods in the Java Card world. Java Card is a technology that provides means to program smart (chip) cards with (a subset of) the Java language. The use of formal methods in the Java Card context is highly justified due to the criticality of Java Card applications. First of all, Java Card applications are usually security critical (e.g., authentication, electronic cash), second, they are cost critical (i.e. they are distributed in large amounts making updates quite difficult) and finally, they can also be legally critical (e.g., when the digital signature law is considered). Thus the robustness and correctness of Java Card applications should be enforced by the best means possible, i.e. by the use of formal verification techniques. At the same time Java Card seems to be a good target for formal verification - due tothe relative simplicity of Java Card applications (as compared to full Java), formal verification becomes a feasible and manageable task. In this thesis, we touch upon different levels of Java Card application development and the use of formal methods. We start by defining a UML/OCL supported development process specifically tailored to JavaCard applications, then we go on to define an extension to the logic used in formal verification of Java Card programs to handle so called "rip out" properties (properties that should be maintained in case of an unexpected termination of a Java Card program), which are specific to Java Card. Finally, we end up with a simple tool support for Java Card program compilation and testing inside a CASE tool. The thesis contains three papers focusing on these aspects. The main purpose of this work is to ensure the robustness of Java Card applications by providing a well defined development process and means to formally verify properties specific to Java Card applications to be able to develop Java Card applets which are robust "by design". At the sametime we want to make rigorous Java Card development relatively easy, tool supported (automated wherever possible) and usable by people that do not have years of training in formal methods.
|
|
| 30. |
- Mostowski, Wojciech, 1976-
(författare)
-
Verifying Java Card Programs
- 2016
-
Ingår i: Deductive Software Verification – The KeY Book. - Heidelberg : Springer. - 9783319498119 - 9783319498126 ; , s. 353-380
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- This chapter presents the extension of KeY and JavaDL to handle a particular and peculiar dialect of Java, namely Java Card, for programming smart cards. The necessary extensions to the logic and the specification language are discussed, followed by a number of small case studies. The chapter is concluded with applications of the ideas presented here to on-going and future research, in particular in reasoning about concurrent Java programs. © Springer International Publishing AG 2016
|
|
| 31. |
- Varshosaz, Mahsa, 1985-
(författare)
-
Modeling and Model-Based Testing of Software Product Lines
- 2019
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Software product line (SPL) engineering has become common practice for mass production and customization of variability intensive systems. A software product line comprises a family of software systems which share a managed core set of artifacts and also have a set of well-defined variabilities. The main idea in SPL engineering is to enable systematic reuse in different phases of software development to reduce cost and time to release.Model-Based Testing (MBT) is a technique that is widely used for quality assurance of software systems. In MBT, an abstract model, which captures the desired behavior of the system, is used to generate test cases. The test cases are executed against a real implementation of the system and the conformance between the implementation and the specification is checked by comparing the observed outputs with the ones prescribed by the model.Software product lines have been applied in a number of domains with mission critical systems. MBT is one of the techniques that has been used for analysis of such systems. As the number of products can be potentially large in an SPL, using conventional approaches for MBT of the products of an SPL individually can be very costly and time consuming. To tackle this problem, several approaches have been proposed in order to enable systematic reuse in different phases of the MBT process.An efficient modeling technique is the first step towards an efficient MBT technique for SPLs. So far, several formalisms have been proposed for modeling SPLs. In this thesis, we conduct a study on such modeling techniques, focusing on four fundamental formalisms, namely featured transition systems, modal transition systems, product line calculus of communicating systems, and 1- selecting modal transition systems. We compare the expressive power and the succinctness of these formalisms.Furthermore, we investigate adapting existing MBT methods for efficient testing of SPLs. As a part of this line of our research, we adapt the test case generation algorithm of one of the well-known black-box testing approaches, namely, Harmonized State Identification (HSI) method by exploiting the idea of delta-oriented programming. We apply the adapted test case generation algorithm to a case study taken from industry and the results show up to 50 percent reduction of time in test case generation by using the delta-oriented HSI method.In line with our research on investigating existing MBT techniques, we compare the relative efficiency and effectiveness of the test case generation algorithms of the well-known Input-Output Conformance (ioco) testing approach and the complete ioco which is another testing technique used for input output transition systems that guarantees fault coverage. The comparison is done using three case studies taken from the automotive and railway domains. The obtained results show that complete ioco is more efficient in detecting deep faults (i.e., the faults reached through longer traces) in large state spaces while ioco is more efficient in detecting shallow faults (i.e., the faults reached through shorter traces) in small state spaces.Moreover, we conduct a survey on sampling techniques, which have been proposed as a solution for handling the large number of products in analysis. In general, in product sampling a subset of products that collectively cover the behavior of the product line are selected. Performing tests on well selected sample set can reveal most of the faults in all products. We provide a classification for a catalog of studies on product sampling for software product lines. Additionally, we present a number of insights on the studied work as well as gaps for the future research.
|
|
