| 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.
|
|
