hh.sePublications
Change search
Link to record
Permanent link

Direct link
Mostowski, Wojciech
Publications (10 of 18) Show all publications
Entekhabi, S., Mostowski, W. & Mousavi, M. R. (2023). Automated and Efficient Test-Generation for Grid-Based Multiagent Systems: Comparing Random Input Filtering versus Constraint Solving. ACM Transactions on Software Engineering and Methodology, 33(1), Article ID 12.
Open this publication in new window or tab >>Automated and Efficient Test-Generation for Grid-Based Multiagent Systems: Comparing Random Input Filtering versus Constraint Solving
2023 (English)In: ACM Transactions on Software Engineering and Methodology, ISSN 1049-331X, E-ISSN 1557-7392, Vol. 33, no 1, article id 12Article in journal (Refereed) Published
Abstract [en]

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

Place, publisher, year, edition, pages
New York, NY: Association for Computing Machinery (ACM), 2023
Keywords
autonomous agents, constraint solving, domain specific languages, grid-based systems, multiagent systems, test input filtering, Test input generation, test selection
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-52732 (URN)10.1145/3624736 (DOI)2-s2.0-85183761518 (Scopus ID)
Available from: 2024-02-21 Created: 2024-02-21 Last updated: 2024-04-30Bibliographically approved
Mostowski, W. (2022). Implications of Deductive Verification on Research Quality: Field Study. In: Wolfgang Ahrendt; Bernhard Beckert; Richard Bubel; Einar Broch Johnsen (Ed.), The Logic of Software. A Tasting Menu of Formal Methods: Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday (pp. 370-381). Cham: Springer, 13360 LNCS
Open this publication in new window or tab >>Implications of Deductive Verification on Research Quality: Field Study
2022 (English)In: The Logic of Software. A Tasting Menu of Formal Methods: Essays Dedicated to Reiner Hähnle on the Occasion of His 60th Birthday / [ed] Wolfgang Ahrendt; Bernhard Beckert; Richard Bubel; Einar Broch Johnsen, Cham: Springer, 2022, Vol. 13360 LNCS, p. 370-381Chapter in book (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Cham: Springer, 2022
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) ; 13360
National Category
Software Engineering
Identifiers
urn:nbn:se:hh:diva-49331 (URN)10.1007/978-3-031-08166-8_17 (DOI)2-s2.0-85133651624 (Scopus ID)978-3-031-08165-1 (ISBN)978-3-031-08166-8 (ISBN)
Available from: 2023-01-11 Created: 2023-01-11 Last updated: 2023-01-11Bibliographically approved
Entekhabi, S., Mostowski, W., Mousavi, M. R. & Arts, T. (2022). Locality-Based Test Selection for Autonomous Agents. In: Clark D., Menendez H., Cavalli A.R. (Ed.), Testing Software and Systems: 33rd IFIP WG 6.1 International Conference on Testing Software Systems, ICTSS 2021, London, UK, November 10-12, 2021 Proceedings. Paper presented at 33rd IFIP WG 6.1 International Conference on Testing Software Systems, ICTSS 2021, 10 November 2021 through 12 November 2021, , 277709, 2022 (pp. 73-89). Springer Science+Business Media B.V., 13045
Open this publication in new window or tab >>Locality-Based Test Selection for Autonomous Agents
2022 (English)In: Testing Software and Systems: 33rd IFIP WG 6.1 International Conference on Testing Software Systems, ICTSS 2021, London, UK, November 10-12, 2021 Proceedings / [ed] Clark D., Menendez H., Cavalli A.R., Springer Science+Business Media B.V., 2022, Vol. 13045, p. 73-89Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Springer Science+Business Media B.V., 2022
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 13045
Keywords
Autonomous agents, Domain specific languages, Model-based testing, Scenario-based testing, Test input generation, Test selection
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-49111 (URN)10.1007/978-3-031-04673-5_6 (DOI)000870696000006 ()2-s2.0-85130232932 (Scopus ID)9783031046728 (ISBN)
Conference
33rd IFIP WG 6.1 International Conference on Testing Software Systems, ICTSS 2021, 10 November 2021 through 12 November 2021, , 277709, 2022
Available from: 2023-01-05 Created: 2023-01-05 Last updated: 2024-04-30Bibliographically approved
Sidorenko, G., Mostowski, W., Vinel, A., Sjöberg, J. & Cooney, M. (2021). The CAR Approach: Creative Applied Research Experiences for Master’s Students in Autonomous Platooning. In: 2021 30th IEEE International Conference on Robot and Human Interactive Communication, RO-MAN 2021: . Paper presented at 30th IEEE International Conference on Robot and Human Interactive Communication, RO-MAN 2021, Virtual, Vancouver, BC, Canada, 08-12/08, 2021 (pp. 214-221). IEEE
Open this publication in new window or tab >>The CAR Approach: Creative Applied Research Experiences for Master’s Students in Autonomous Platooning
Show others...
2021 (English)In: 2021 30th IEEE International Conference on Robot and Human Interactive Communication, RO-MAN 2021, IEEE, 2021, p. 214-221Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
IEEE, 2021
National Category
Pedagogy
Identifiers
urn:nbn:se:hh:diva-46083 (URN)10.1109/RO-MAN50785.2021.9515560 (DOI)000709817200031 ()2-s2.0-85115115499 (Scopus ID)978-1-6654-0492-1 (ISBN)978-1-6654-4637-2 (ISBN)
Conference
30th IEEE International Conference on Robot and Human Interactive Communication, RO-MAN 2021, Virtual, Vancouver, BC, Canada, 08-12/08, 2021
Available from: 2021-12-13 Created: 2021-12-13 Last updated: 2023-10-05Bibliographically approved
Mostowski, W. (2020). From Explicit to Implicit Dynamic Frames in Concurrent Reasoning for Java. In: Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Mattias Ulbrich (Ed.), Deductive Software Verification: Future Perspectives (pp. 177-203). Heidelberg: Springer
Open this publication in new window or tab >>From Explicit to Implicit Dynamic Frames in Concurrent Reasoning for Java
2020 (English)In: Deductive Software Verification: Future Perspectives / [ed] Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Mattias Ulbrich, Heidelberg: Springer, 2020, p. 177-203Chapter in book (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Heidelberg: Springer, 2020
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 12345
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-43704 (URN)10.1007/978-3-030-64354-6_7 (DOI)2-s2.0-85097580783 (Scopus ID)
Funder
Knowledge Foundation, 280034
Available from: 2020-12-15 Created: 2020-12-15 Last updated: 2021-01-12Bibliographically approved
David, J., Mostowski, W., Aramrattana, M., Fan, Y., Varshosaz, M., Karlsson, P., . . . Andersson, E. (2019). Design and Development of a Hexacopter for the Search and Rescue of a Lost Drone. In: : . Paper presented at IROS 2019 - Workshop on Challenges in Vision-based Drones Navigation, Macau, China, November 8, 2019.
Open this publication in new window or tab >>Design and Development of a Hexacopter for the Search and Rescue of a Lost Drone
Show others...
2019 (English)Conference paper, Published paper (Refereed)
Abstract [en]

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.

Keywords
drones, UAV, competition, search and rescue
National Category
Robotics and automation
Identifiers
urn:nbn:se:hh:diva-40830 (URN)
Conference
IROS 2019 - Workshop on Challenges in Vision-based Drones Navigation, Macau, China, November 8, 2019
Available from: 2019-11-04 Created: 2019-11-04 Last updated: 2025-02-09Bibliographically approved
Mostowski, W. (2019). Model-based fault injection for testing gray-box systems. The Journal of logical and algebraic methods in programming, 103, 31-45
Open this publication in new window or tab >>Model-based fault injection for testing gray-box systems
2019 (English)In: The Journal of logical and algebraic methods in programming, ISSN 2352-2208, E-ISSN 2352-2216, Vol. 103, p. 31-45Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
Amsterdam: Elsevier, 2019
Keywords
Model-based testing, Fault injection, Fault models, Multi-purpose models, Functional testing, Robustness testing
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-38438 (URN)10.1016/j.jlamp.2018.10.003 (DOI)000458714300002 ()2-s2.0-85065766503 (Scopus ID)
Projects
AUTO-CAAS
Funder
Knowledge Foundation
Available from: 2018-11-28 Created: 2018-11-28 Last updated: 2020-08-28Bibliographically approved
Ernst, G., Huisman, M., Mostowski, W. & Ulbrich, M. (2019). VerifyThis – Verification Competition with a Human Factor. Paper presented at 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Prague, Czech Republic, April 6–11, 2019. Lecture Notes in Computer Science, 11429, 176-195
Open this publication in new window or tab >>VerifyThis – Verification Competition with a Human Factor
2019 (English)In: Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349, Vol. 11429, p. 176-195Article in journal (Refereed) Published
Abstract [en]

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

Place, publisher, year, edition, pages
Heidelberg: Springer, 2019
Keywords
Verify This, Program verification, Specification languages, Tool development, Competition
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-41109 (URN)10.1007/978-3-030-17502-3_12 (DOI)000681183400012 ()2-s2.0-85064931936 (Scopus ID)978-3-030-17501-6 (ISBN)978-3-030-17502-3 (ISBN)
Conference
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Prague, Czech Republic, April 6–11, 2019
Available from: 2019-12-04 Created: 2019-12-04 Last updated: 2023-08-21Bibliographically approved
Aichernig, B. K., Mostowski, W., Mousavi, M. R., Tappler, M. & Taromirad, M. (2018). Model Learning and Model-Based Testing. In: Amel Bennaceur, Reiner Hähnle, Karl Meinke (Ed.), Amel Bennaceur, Reiner Hähnle, Karl Meinke (Ed.), Machine Learning for Dynamic Software Analysis: Potentials and Limits. Paper presented at Machine Learning for Dynamic Software Analysis: Potentials and Limits, International Dagstuhl Seminar 16172, Wadern, Germany, April 24-27, 2016 (pp. 74-100). Heidelberg: Springer
Open this publication in new window or tab >>Model Learning and Model-Based Testing
Show others...
2018 (English)In: Machine Learning for Dynamic Software Analysis: Potentials and Limits / [ed] Amel Bennaceur, Reiner Hähnle, Karl Meinke, Heidelberg: Springer, 2018, p. 74-100Conference paper, Published paper (Refereed)
Abstract [en]

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

Place, publisher, year, edition, pages
Heidelberg: Springer, 2018
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 11026
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-38437 (URN)10.1007/978-3-319-96562-8_3 (DOI)000476941200003 ()2-s2.0-85051109384 (Scopus ID)978-3-319-96561-1 (ISBN)978-3-319-96562-8 (ISBN)
Conference
Machine Learning for Dynamic Software Analysis: Potentials and Limits, International Dagstuhl Seminar 16172, Wadern, Germany, April 24-27, 2016
Funder
Knowledge Foundation
Available from: 2018-11-28 Created: 2018-11-28 Last updated: 2021-05-19Bibliographically approved
Aramrattana, M., Detournay, J., Englund, C., Frimodig, V., Jansson, O. U., Larsson, T., . . . Shahanoor, G. (2018). Team Halmstad Approach to Cooperative Driving in the Grand Cooperative Driving Challenge 2016. IEEE transactions on intelligent transportation systems (Print), 19(4), 1248-1261
Open this publication in new window or tab >>Team Halmstad Approach to Cooperative Driving in the Grand Cooperative Driving Challenge 2016
Show others...
2018 (English)In: IEEE transactions on intelligent transportation systems (Print), ISSN 1524-9050, E-ISSN 1558-0016, Vol. 19, no 4, p. 1248-1261Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
Piscataway, N.J.: Institute of Electrical and Electronics Engineers Inc., 2018
Keywords
Adaptive cruise control, Cruise control, Decision making, Autonomous driving, Cooperative adaptive cruise control, Cooperative driving, GCDC 2016, IEEE 802.11p, platooning, Cooperative communication
National Category
Computer and Information Sciences Software Engineering
Identifiers
urn:nbn:se:hh:diva-38712 (URN)10.1109/TITS.2017.2752359 (DOI)000429017300023 ()2-s2.0-85041535321 (Scopus ID)
Available from: 2019-01-08 Created: 2019-01-08 Last updated: 2021-05-17Bibliographically approved
Organisations

Search in DiVA

Show all publications