CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Graphical editing support for QuickCheck models

T. Arts ; K. Bogdanov ; Alex Gerdes (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; John Hughes (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
2015 IEEE 8th International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2015 - Proceedings (2159-4848). (2015)
[Konferensbidrag, refereegranskat]

QuickCheck can test a system by specifying a state machine for the API exported by that system. This state machine specification includes a list of possible API calls. Each call is accompanied by a precondition, a postcondition, a generator for the arguments, and a description of how the state is changed. Based on this specification QuickCheck generates a random sequence of API calls. The preconditions ensure that a generated sequence is valid, and the postconditions check that the system behaves as expected. Many systems require an initialisation call before other calls, describing the transition from an uninitialized to an initialised state. QuickCheck offers two ways of specifying transitions between states: using preconditions or a finite state machine abstraction. In this paper we show, by means of an example, that the latter approach is to be preferred. In addition, we present a recent extension to QuickCheck that allows a user to graphically create and edit a finite state machine specification. This extension simplifies and speeds up the specification of a finite state machine, which can be regarded as a formal model of the system, considerably. The graphical representation makes the formal model easier to understand, and visualises the distribution of API calls. Moreover, the extension allows the user to change this distribution.



Denna post skapades 2015-07-21. Senast ändrad 2016-06-29.
CPL Pubid: 219898

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)