hh.sePublications
Change search
Link to record
Permanent link

Direct link
BETA
Mostowski, Wojciech
Publications (10 of 10) Show all publications
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)
Projects
AUTO-CAAS
Funder
Knowledge Foundation
Available from: 2018-11-28 Created: 2018-11-28 Last updated: 2019-02-05Bibliographically 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)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: 2018-12-11Bibliographically 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: 2019-01-08Bibliographically approved
Mostowski, W., Arts, T. & Hughes, J. (2017). Modelling of Autosar Libraries for Large Scale Testing. In: Holger Hermanns & Peter Höfner (Ed.), 2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017): . Paper presented at 2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017), Uppsala, Sweden, 29th April, 2017 (pp. 184-199). , 244
Open this publication in new window or tab >>Modelling of Autosar Libraries for Large Scale Testing
2017 (English)In: 2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017) / [ed] Holger Hermanns & Peter Höfner, 2017, Vol. 244, p. 184-199Conference paper, Published paper (Refereed)
Abstract [en]

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.

Series
Electronic Proceedings in Theoretical Computer Science
Keywords
model-based testing, API compliance, Autosar, QuickCheck, Erlang
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-35404 (URN)10.4204/EPTCS.244.7 (DOI)000405454300008 ()2-s2.0-85018894179 (Scopus ID)
Conference
2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017), Uppsala, Sweden, 29th April, 2017
Projects
AUTO-CAAS
Funder
Knowledge Foundation
Available from: 2017-11-13 Created: 2017-11-13 Last updated: 2018-01-13Bibliographically approved
Huisman, M., Monahan, R., Müller, P., Mostowski, W. & Ulbrich, M. (2017). VerifyThis 2017: A Program Verification Competition. Karlsruhe: Karlsruhe Institute of Technology
Open this publication in new window or tab >>VerifyThis 2017: A Program Verification Competition
Show others...
2017 (English)Report (Other academic)
Abstract [en]

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.

Place, publisher, year, edition, pages
Karlsruhe: Karlsruhe Institute of Technology, 2017. p. 9
Series
Karlsruhe Reports in Informatics, ISSN 2190-4782 ; 10
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-35742 (URN)10.5445/ir/1000077160 (DOI)
Available from: 2017-12-05 Created: 2017-12-05 Last updated: 2018-01-13Bibliographically approved
Mostowski, W. & Ulbrich, M. (2016). Dynamic Dispatch for Method Contracts Through Abstract Predicates. Paper presented at 15th International Conference on Modularity (MODULARITY'15), Fort Collins, Colorado, USA, March 16-19, 2015. Lecture Notes in Computer Science, 9800, 238-267
Open this publication in new window or tab >>Dynamic Dispatch for Method Contracts Through Abstract Predicates
2016 (English)In: Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349, Vol. 9800, p. 238-267Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
Cham: Springer, 2016
Keywords
Modular specification, Design by Contract, Dynamic dispatch, abstract predicates, JML
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-32127 (URN)10.1007/978-3-319-46969-0_7 (DOI)2-s2.0-84992727403 (Scopus ID)
Conference
15th International Conference on Modularity (MODULARITY'15), Fort Collins, Colorado, USA, March 16-19, 2015
Projects
VerCorsAUTO-CAAS
Funder
Knowledge Foundation
Note

Funding: ERC grant 258405 for the VerCors project and by the Swedish Knowledge Foundation grant for the project AUTO-CAAS, DFG (German Research Foundation) under the Priority Programme SPP1593: Design For Future – Managed Software Evolution.

Available from: 2016-10-03 Created: 2016-10-03 Last updated: 2018-03-23Bibliographically approved
Mostowski, W. (2016). Dynamic Frames Based Verification Method for Concurrent Java Programs. In: Arie Gurfinkel & Sanjit A. Seshia (Ed.), Verified Software: Theories, Tools, and Experiments: 7th International Conference, VSTTE 2015, San Francisco, CA, USA, July 18-19, 2015. Revised Selected Papers. Paper presented at 7th International Conference, VSTTE 2015, San Francisco, CA, USA, July 18-19, 2015 (pp. 124-141). New York: Springer International Publishing Switzerland, 9593
Open this publication in new window or tab >>Dynamic Frames Based Verification Method for Concurrent Java Programs
2016 (English)In: Verified Software: Theories, Tools, and Experiments: 7th International Conference, VSTTE 2015, San Francisco, CA, USA, July 18-19, 2015. Revised Selected Papers / [ed] Arie Gurfinkel & Sanjit A. Seshia, New York: Springer International Publishing Switzerland , 2016, Vol. 9593, p. 124-141Conference paper, Published paper (Refereed)
Abstract [en]

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

Place, publisher, year, edition, pages
New York: Springer International Publishing Switzerland, 2016
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9593
National Category
Computer Systems
Identifiers
urn:nbn:se:hh:diva-30171 (URN)10.1007/978-3-319-29613-5_8 (DOI)000374049000008 ()2-s2.0-84958954011 (Scopus ID)978-3-319-29612-8 (ISBN)978-3-319-29613-5 (ISBN)
Conference
7th International Conference, VSTTE 2015, San Francisco, CA, USA, July 18-19, 2015
Projects
VerCorsAUTO-CAAS
Funder
Knowledge Foundation
Note

This work is supported by ERC grant 258405 for the VerCors project and by the Swedish Knowledge Foundation grant for the AUTO-CAAS project.

Available from: 2016-01-14 Created: 2016-01-14 Last updated: 2018-03-22Bibliographically approved
Kunze, S., Mostowski, W., Mousavi, M. R. & Varshosaz, M. (2016). Generation of Failure Models through Automata Learning. In: Proceedings: 2016 Workshop on Automotive Systems/Software Architectures. Paper presented at Workshop on Automotive Systems/Software Architectures (WASA 2016), Venice, Italy, 5-8 April, 2016 (pp. 22-25). Los Alamitos: IEEE Computer Society, Article ID 7484118.
Open this publication in new window or tab >>Generation of Failure Models through Automata Learning
2016 (English)In: Proceedings: 2016 Workshop on Automotive Systems/Software Architectures, Los Alamitos: IEEE Computer Society, 2016, p. 22-25, article id 7484118Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Los Alamitos: IEEE Computer Society, 2016
Keywords
model-based testing, automatic test generation, automata learning, failure model, AUTOSAR
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-32126 (URN)10.1109/WASA.2016.7 (DOI)000386759300006 ()2-s2.0-84978245358 (Scopus ID)978-1-5090-2571-8 (ISBN)
Conference
Workshop on Automotive Systems/Software Architectures (WASA 2016), Venice, Italy, 5-8 April, 2016
Projects
AUTO-CAASEFFEMBAC
Funder
Knowledge FoundationSwedish Research Council
Available from: 2016-10-03 Created: 2016-10-03 Last updated: 2018-03-23Bibliographically approved
Grahl, D., Bubel, R., Mostowski, W., Schmitt, P. H., Ulbrich, M. & Weiß, B. (2016). Modular Specification and Verification. In: Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt & Mattias Ulbrich (Ed.), Deductive Software Verification – The KeY Book: From Theory to Practice (pp. 289-351). Heidelberg: Springer
Open this publication in new window or tab >>Modular Specification and Verification
Show others...
2016 (English)In: Deductive Software Verification – The KeY Book: From Theory to Practice / [ed] Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt & Mattias Ulbrich, Heidelberg: Springer, 2016, p. 289-351Chapter in book (Other academic)
Abstract [en]

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.

Place, publisher, year, edition, pages
Heidelberg: Springer, 2016
Series
Lecture Notes in Computer Science (LNCS), ISSN 0302-9743 ; 10001
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-35405 (URN)10.1007/978-3-319-49812-6_9 (DOI)2-s2.0-85006997785 (Scopus ID)978-3-319-49811-9 (ISBN)978-3-319-49812-6 (ISBN)
Available from: 2017-11-13 Created: 2017-11-13 Last updated: 2018-01-13Bibliographically approved
Mostowski, W. (2016). Verifying Java Card Programs. In: Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt & Mattias Ulbrich (Ed.), Deductive Software Verification – The KeY Book: From Theory to Practice (pp. 353-380). Heidelberg: Springer
Open this publication in new window or tab >>Verifying Java Card Programs
2016 (English)In: Deductive Software Verification – The KeY Book: From Theory to Practice / [ed] Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt & Mattias Ulbrich, Heidelberg: Springer, 2016, p. 353-380Chapter in book (Other academic)
Abstract [en]

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

Place, publisher, year, edition, pages
Heidelberg: Springer, 2016
Series
Lecture Notes in Computer Science (LNCS), ISSN 0302-9743 ; 10001
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-35406 (URN)10.1007/978-3-319-49812-6_10 (DOI)2-s2.0-85006990515 (Scopus ID)978-3-319-49811-9 (ISBN)978-3-319-49812-6 (ISBN)
Available from: 2017-11-13 Created: 2017-11-13 Last updated: 2018-01-13Bibliographically approved
Organisations

Search in DiVA

Show all publications