Modelling of Autosar Libraries for Large Scale Testing
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...
Main Authors: | , , |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2017-03-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1703.06574v1 |
id |
doaj-db376f57f8594088839aba2d2b8600e2 |
---|---|
record_format |
Article |
spelling |
doaj-db376f57f8594088839aba2d2b8600e22020-11-25T02:43:14ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802017-03-01244Proc. MARS 201718419910.4204/EPTCS.244.7:3Modelling of Autosar Libraries for Large Scale TestingWojciech Mostowski0Thomas Arts1John Hughes2 Halmstad University, Sweden Quviq AB, Sweden Chalmers University of Technology and Quviq AB, Sweden 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.http://arxiv.org/pdf/1703.06574v1 |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
Wojciech Mostowski Thomas Arts John Hughes |
spellingShingle |
Wojciech Mostowski Thomas Arts John Hughes Modelling of Autosar Libraries for Large Scale Testing Electronic Proceedings in Theoretical Computer Science |
author_facet |
Wojciech Mostowski Thomas Arts John Hughes |
author_sort |
Wojciech Mostowski |
title |
Modelling of Autosar Libraries for Large Scale Testing |
title_short |
Modelling of Autosar Libraries for Large Scale Testing |
title_full |
Modelling of Autosar Libraries for Large Scale Testing |
title_fullStr |
Modelling of Autosar Libraries for Large Scale Testing |
title_full_unstemmed |
Modelling of Autosar Libraries for Large Scale Testing |
title_sort |
modelling of autosar libraries for large scale testing |
publisher |
Open Publishing Association |
series |
Electronic Proceedings in Theoretical Computer Science |
issn |
2075-2180 |
publishDate |
2017-03-01 |
description |
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. |
url |
http://arxiv.org/pdf/1703.06574v1 |
work_keys_str_mv |
AT wojciechmostowski modellingofautosarlibrariesforlargescaletesting AT thomasarts modellingofautosarlibrariesforlargescaletesting AT johnhughes modellingofautosarlibrariesforlargescaletesting |
_version_ |
1724770676671250432 |