CPN SIMULATION-BASED TEST CASE GENERATION ......A utilização de testes baseados em modelos (MBT) apresenta-se como alternativa para solução destes problemas, através do uso de

BRUNO CESAR FERREIRA SILVA

CPN SIMULATION-BASED TEST CASE GENERATION FROMNATURAL LANGUAGE REQUIREMENTS

Universidade Federal de Pernambuco

[email protected]

www.cin.ufpe.br/~posgraduacao

RECIFE2016

www.cin.ufpe.br/~posgraduacao

Bruno Cesar Ferreira Silva


M.Sc. Dissertation presented to the Centro de Informática

of Universidade Federal de Pernambuco in partial fulfilment

of the requirements for the degree of Master of Science in

Computer Science.

Supervisor: Augusto Sampaio (UFPE, Brazil)Co-Supervisor: Gustavo Carvalho (UPE, Brazil)

RECIFE2016

Catalogação na fonte

Bibliotecária Monick Raquel Silvestre da S. Portes, CRB4-1217

S586c Silva, Bruno Cesar Ferreira

CPN simulation-based test case generation from natural language requirements / Bruno Cesar Ferreira Silva. – 2016.

62 f.: il., fig., tab. Orientador: Augusto Sampaio. Dissertação (Mestrado) – Universidade Federal de Pernambuco. CIn,

Ciência da Computação, Recife, 2016. Inclui referências e apêndices.

1. Ciência da computação. 2. Redes de Petri. 3. Simulação de modelos. I. Silva, Bruno Cesar Ferreira (orientador). II. Título. 004 CDD (23. ed.) UFPE- MEI 2017-27

Bruno Cesar Ferreira Silva


Dissertação de Mestrado apresentada ao Programa de Pós-Graduação emCiência da Computação da UniversidadeFederal de Pernambuco, como requisitoparcial para a obtenção do título de Mestreem Ciência da Computação

Aprovado em: 05/09/2016.

BANCA EXAMINADORA

__________________________________________Prof. Dr. Eduardo Antônio Guimarães Tavares

Centro de Informática / UFPE

__________________________________________Prof. Dr. Jorge Cesar Abrantes de Figueiredo

Departamento de Sistemas e Computação / UFCG

__________________________________________Prof. Dr. Augusto Cezar Alves Sampaio

Centro de Informática / UFPE(Orientador)

I dedicate this master thesis to my mother, my wife, my

children and professors who gave me the necessary support

to get here.

Acknowledgements

I would like to thank some people who have contributed to the achievement of the resultspresented in this paper. In addition to my supervisors, other teachers of the Centro de Informáticaat Universidade Federal de Pernambuco provided me the necessary background in the topicscovered; among them, i would like to mention Professor Eduardo Tavares, Professor FernandoCastor, and Professor Alexandre Mota. Regarding the company where I work, I would alsodedicate a special thanks to Adelia Mangelli the trust and support, recognizing the importance ofthe work that would be developed.

The journey was undertaken would not be possible without the participation of theother two authors of this paper. I have the most sincere gratitude for my latest idols, ProfessorAugusto Sampaio and Professor Gustavo Carvalho. They were tireless, highly competent, gentleand human in the development of this work. I received them the necessary motivation andencouragement in the most difficult moments.

No one was so important as my family and my best friends forever. Swami Nogueiraand Pompeu Jácome Lima (my dear friends) for the moments of entertainment and reflections,conveying his wise words. João Carlos and Maria Cristina (my dear father and mother-in-law)for transmitting its tranquillity.

Finally, but not least, Samanta Della Bella (my wife, buddy and support) for her under-standing, competence and sensitivity. Bruna, Stella, Gustavo and Riva (my darling children andmotivation) who encouraged me to never give up. And, above all, God.

Abstract

Software Engineering faces challenges such as difficulty in understanding the user needs, am-biguous specifications, poorly defined requirements and therefore problems in interpreting thesystem requirements. Model-based testing (MBT) is presented as an alternative for solvingthese problems by using (semi-)formal methods, in the specification, modelling or analysis ofrequirements, as well as by automatically generating test cases.This work proposes and implements a test generation strategy from Natural Language (NL)requirements via translation into Coloured Petri Nets (CPN), an extension of Petri Nets thatsupports model structuring. This strategy extends previous work on the NAT2TEST framework,which involves syntactic and semantic analyses of NL requirements and the generation of Data-Flow Reactive System (DFRS) as an intermediate representation, from which target formalmodels can be obtained for the purpose of test case generation. Our contributions include asystematic translation of DFRSs into CPN models, besides a strategy for test generation. Weillustrate our overall approach with a running example.Therefore, this work presents a variant for the NATural Language Requirements to TEST Cases(NAT2TEST) strategy, in which the Coloured Petri Nets (CPN) is used as an intermediate model.The NAT2TEST strategy, which is applicable to discrete or continuous systems, consists of fivephases: syntactic and semantic analyses, DFRS generation, CPN generation, and generation oftest cases. The approach proposed here, which is based on Petri Nets simulation, has as benefitthe maturity of the theory and tools related to CPN. Moreover, there are available resources foranalysing structural and behavioural properties of the model. The process is automated by theNAT2TEST tool until the DFRS generation. The model translation from the DFRS to the CPNis automated by Spoofax framework. Finally, the test cases generation occurs automatically viasimulations held in the CPN Tools.Our strategy was evaluated considering examples from the literature (Vending Machine andNuclear Power Plant) and the aerospace industry (Priority Control). We analysed performanceand the ability to detect defects generated via mutation. In general, our strategy outperformedthe considered baseline: random testing. We also compared our strategy with the CSP version.

Keywords: Model-based testing. Controlled natural language. Data-flow reactive system.Automatic test generation. Coloured Petri nets. Simulation of models.

Resumo

A Engenharia de Software possui desafios clássicos como dificuldade no entendimento das neces-sidades dos usuários, especificações ambíguas, requisitos mal definidos e, portanto, problemasna interpretação destes. A utilização de testes baseados em modelos (MBT) apresenta-se comoalternativa para solução destes problemas, através do uso de métodos (semi-)formais, seja naespecificação, modelagem ou análises de requisitos, bem como na geração automática de casosde testes.Este trabalho propõe e implementa uma estratégia de geração de testes a partir de requisitosescritos em linguagem natural (NL) através da tradução para modelos em Redes de Petri Colorida(CPN), uma extensão de Redes de Petri que incorpora estruturação de modelos. Esta estratégiaestende um trabalho anterior (NAT2TEST framework), que envolve análises sintática e semânticade requisitos em linguagem natural (NL) e geração do modelo de sistemas reativos baseados emfluxos de dados (DFRS) como uma representação intermediária, a partir do qual outros modelosformais podem ser obtidos com o propósito de geração de casos de testes. Nossa contribuiçãoinclui uma tradução sistemática de DFRSs para modelos CPN, assim como uma estratégia parageração de testes. Ilustramos nossa abordagem através de um exemplo prático.Assim sendo, este trabalho apresenta uma variante da estratégia NAT2TEST, na qual formalismointermediário é Redes de Petri Colorida (CPN), sendo aplicável a sistemas discretos e contínuos,e que consiste de cinco etapas: análises sintática e semântica, gerações dos modelos DFRS eCPN e de casos de testes. A abordagem empregada, através da simulação de Redes de Petri, temcomo benefícios a maturidade da teoria e das ferramentas associadas a CPN, além de permitir aanálise de propriedades estruturais e comportamentais do modelo. A ferramenta NAT2TEST jáautomatiza a tradução de requisitos em linguagem natural na notação do DFRS. A tradução domodelo DFRS para o formalismo CPN é uma primeira contribuição do presente trabalho e foiautomatizada através do ambiente Spoofax. A geração dos casos de testes foi desenvolvida, deforma automatizada, através de simulações realizadas na ferramenta CPN Tools.A estratégia aqui proposta foi avaliada considerando exemplos da literatura (Vending Machine(VM) e Nuclear Power Plant (NPP)) e da indústria aeroespacial (Priority Control (PC)). Foramanalisados o desempenho e a capacidade de detectar defeitos gerados através de operadores demutação. Em geral, a nossa estratégia apresentou melhores resultados do que a referência adotada:testes aleatórios. A estratégia também foi comparada com a versão que utiliza CommunicatingSequential Processes (CSP) como modelo formal intermediário e apresentou melhor desempenhonos três estudos realizados. Em um deles, encontrou a mesma quantidade de defeitos, sendosuperior nos demais.

Palavras-chave: Testes baseados em modelos. Linguagem natural controlada. Sistemas

reativos baseados em fluxos de dados. Geração automática de testes. Redes de Petri coloridas.Simulação de modelos.

List of Figures

2.1 The VM abstract representation . . . . . . . . . . . . . . . . . . . . . . . . . . 202.2 Example of VM signals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 202.3 NAT2TEST strategy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 212.4 An example of a Coloured Petri Net (CPN) . . . . . . . . . . . . . . . . . . . 26

3.1 Page created to represent the requirement REQ001 . . . . . . . . . . . . . . . 313.2 Part of the eXtensible Markup Language (XML) representation of the DFRS for

the VM example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 343.3 DFRS grammar . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 353.4 The rule create-cpn-inputs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 363.5 The rule page-reqx . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37

4.1 Page created to generate the inputs randomly . . . . . . . . . . . . . . . . . . 394.2 Page created to deal with no system reaction . . . . . . . . . . . . . . . . . . . 404.3 Page created to save the test cases in a Comma-separated values (CSV) file . . 414.4 Page created to represent the requirement REQ002 . . . . . . . . . . . . . . . 424.5 Generating random inputs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 434.6 Processing the initial input by the transition noREQ . . . . . . . . . . . . . . . 44

List of Tables

2.1 Example of a requirement frame for REQ002 (Vending Machine) . . . . . . . . 222.2 Example of test case for REQ002 (Vending Machine) . . . . . . . . . . . . . . 232.3 The variables and types of DFRS for the VM example . . . . . . . . . . . . . . 232.4 The functions of DFRS for the VM example . . . . . . . . . . . . . . . . . . . 24

4.1 Example of a test case for the adapted Vending Machine(VM) . . . . . . . . . 45

5.1 Perfomance Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 475.2 Mutant Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49

6.1 Related work –– modelling timed-systems from NL requirements using CPNs . 53

List of Acronyms

ACT Action . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

AGT Agent . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

AST Abstract Syntax Tree . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

CAC Condition Action . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .22

CFV Condition From Value . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

CMD Condition Modifier . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

CPN Coloured Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

CPT Condition Patient . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

CSP Communicating Sequential Processes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

csptio CSP timed input-output conformance relation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53

CSV Comma-separated values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37

CTV Condition To Value . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

DFRS Data-Flow Reactive System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

DSL Domain-Specific Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28

DTD Document Type Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

IMR Intermediate Model Representation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

MBT Model-based testing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

NAT2TEST NATural Language Requirements to TEST Cases . . . . . . . . . . . . . . . . . . . . . . . . . . 16

NL Natural Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

NLP Natural Language Processing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

NPP Nuclear Power Plant . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49

OCS Output Colour Set . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32

PAT Patient . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

PC Priority Control . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

SUT System Under Test . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

SCR Software Cost Reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .16

SysReq-CNL System Requirements Controlled Natural Language . . . . . . . . . . . . . . . . . . . . . . . 21

TOV To Value . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

VM Vending Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

XML eXtensible Markup Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

Contents

1 Introduction 151.1 Research question . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171.2 Main contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171.3 Organization of the dissertation . . . . . . . . . . . . . . . . . . . . . . . . . . 18

2 Background 192.1 NAT2TEST strategy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 202.2 Data-flow reactive systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . 232.3 Coloured Petri nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 242.4 Spoofax framework . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

3 Translating from DFRS to CPN 303.1 CPN models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

3.1.1 Representing input variables . . . . . . . . . . . . . . . . . . . . . . . 303.1.2 Representing output variables . . . . . . . . . . . . . . . . . . . . . . 313.1.3 Representing functions . . . . . . . . . . . . . . . . . . . . . . . . . . 32

3.2 Systematic translation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 333.2.1 Defining a DFRS grammar . . . . . . . . . . . . . . . . . . . . . . . . 333.2.2 Creating transformation rules . . . . . . . . . . . . . . . . . . . . . . 35

4 Test vectors based on CPN simulation 384.1 Auxiliary components . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38

4.1.1 Generating entries . . . . . . . . . . . . . . . . . . . . . . . . . . . . 384.1.2 Dealing with no system reaction . . . . . . . . . . . . . . . . . . . . . 394.1.3 Creating a test case file . . . . . . . . . . . . . . . . . . . . . . . . . . 404.1.4 Repeated places . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41

4.2 Test vectors generation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 414.2.1 Random inputs generation . . . . . . . . . . . . . . . . . . . . . . . . 424.2.2 System reaction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 434.2.3 Test vectors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43

5 Empirical analysis 465.1 Performance analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 465.2 Mutant-based strength analysis . . . . . . . . . . . . . . . . . . . . . . . . . . 48

6 Conclusion 516.1 Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 516.2 Future work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53

References 55

Appendix 57

A List of requirements 58A.1 Vending machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58A.2 Nuclear power plant . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58A.3 Priority command . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59

B The XML format for .cpn files 60

151515

1Introduction

Since the so-called software crisis (in the sixties), when the term software engineeringwas conceived, difficulty on understanding the user needs, ambiguous specifications, poorlyspecified and interpreted requirements are still common issues. In the field of requirementsengineering, several studies have been conducted focusing on the use of (semi-)formal methodsto specify, model and analyse requirements, besides automatically generating test cases, resultingin greater maturity and in the construction of underlying theories and supporting tools.

Some models can be suitable to prevent ambiguous, missing, contradictory, incorrect,obscured, incomplete requirements. Thus, some techniques, by using models, are applied to helpimprove the quality of systems. Model-based testing (MBT) is an approach based on creating testcases derived from a behaviour model of the System Under Test (SUT). This model describesthe expected behaviour of the test object. These test cases are then, where possible, automaticallygenerated from the test object. The challenge with this approach lies creating a formal behaviourmodel in which the system is represented. According to the Dutch test association TestNet 1,MBT is:

� "Software testing in which a test model is created that describes some of the expectedbehaviour (usually functional) of the test object. The purpose of creating this testmodel is to review the requirements thoroughly and/or to derive test cases in wholeor in part from the test model. The test models are derived from the requirements ordesigns."

Despite the benefits of formal MBT, those who are not familiar with the models syntaxand semantics may be reluctant to adopt theses formalisms. Moreover, most of these models arenot available in the very beginning of the project, when usually natural-language requirementsare available. The model notations may be not easy to interpret by aerospace and automotivedevelopment engineers. Hence, a specialist (usually mathematicians, logicians, computer engi-neers and scientists) is required when such languages, and their corresponding techniques, areused in business contexts.

1www.testnet.org

www.testnet.org

16

One possible alternative to overcome these limitations is to employ Natural LanguageProcessing (NLP) techniques to derive the required models from natural-language specifica-tions automatically. Using NLP techniques to derive formal models from natural-languagerequirements, besides applying MBT techniques, one can reason formally about properties ofspecifications that can be difficult to analyse by means of manual inspection, such as inconsis-tency and incompleteness. A complete NLP system usually counts on five processing levels,depending on its aim: morphological analysis, syntactic analysis, semantic mapping, discourseanalysis and pragmatic analysis.

Concerning MBT, the works ((BODDU et al., 2004), (SNEED, 2007), (SANTIAGO JU-NIOR; VIJAYKUMAR, 2012)) address the joint use of MBT and NLP based on the second andthird NLP levels cited before. There is a trade-off concerning the application of NLP in MBT.Some studies are able to analyse a broad range of sentences, whereas others rely on controlledversions of natural language. The works that adopt the former approach usually depend on ahigher level of user intervention to derive models and to generate test cases. Differently, therestrictions imposed by a Controlled Natural Language (CNL) might allow a more automaticapproach when generating models and test cases. Ideally, a compromise between these two possi-bilities should be sought to provide a useful degree of automation along with a natural-languagespecification feasible to be used in practice.

As formal methods can be used to find errors in requirements, such as inconsistency andincompleteness, they play an important role in the earlier discovery of errors and, thus, reducingcosts and correction efforts (MYERS; SANDLER; BADGETT, 2004). In this light, the strategyNATural Language Requirements to TEST Cases (NAT2TEST) (CARVALHO et al., 2015) wasdevised to generate test cases from natural language requirements. In this strategy, the systembehaviour is formally represented as a Data-Flow Reactive System (DFRS). Then, this modelis translated into a target formalism for generating test cases. The purpose of the NAT2TESTstrategy is to be easily extensible to various target formalisms. The use of CommunicatingSequential Processes (CSP) (CARVALHO; SAMPAIO; MOTA, 2013), Software Cost Reduction(SCR) (CARVALHO et al., 2014) and Intermediate Model Representation (IMR) (CARVALHOet al., 2014) have been explored, considering their particular advantages, but also tailored totheir limitations. For instance, test generation from SCR and IMR is based on commercial tools,which is a practical advantage, but, on the other hand, is not formal in the sense that no explicitconformance relations are adopted. On the other hand, the test strategy for CSP is formal andcan be proved sound, with an explicit conformance notion, and the FDR tool2 is used to generatetest cases as counterexamples of refinement verifications. However, test cases are obtainedvia refinement checking, demanding the complete expansion of the underlying label transitionsystem, which can easily lead to state explosion problems. Concerning the target languages, fromwhich test cases are generated, a comparison is out of the scope of the current work. The purposehere is only to emphasise that models in several different notations can be generated from a

2http://www.cs.ox.ac.uk/projects/fdr/

http://www.cs.ox.ac.uk/projects/fdr/

1.1. RESEARCH QUESTION 17

DFRS. It would be possible to define a testing theory for the DFRS formalism, but this is not thepurpose of the NAT2TEST framework. The idea is use DFRSs just as an intermediate notation,and allow the translation into several target formalisms with their specific testing theories andtool support.

Here we explore the use of Coloured Petri Nets (CPN) as an alternative extension of theNAT2TEST strategy where simulation of CPNs is used for generating test cases. To simulate aCPN model it is not necessary to explore its complete state space first and, thus, we minimisestate space explosion problems. Also, we benefit from the diversity and maturity of CPN tools3.A testing theory based on CPN can also be entirely formal; although our focus here is ondeveloping a first testing strategy that still needs to be proved sound taking into account a suitableconformance relation.

1.1 Research question

In the light of the discussion presented so far, the main research question of this workis: how to efficiently simulate, and generate test cases for timed reactive systems from natural-language requirements? In particular, regarding systems whose behaviour can be described viadata operations and that is time-dependent.

Here, we propose a variant for the formal MBT strategy (NAT2TEST) for generat-ing test cases from natural-language requirements using the formalism (CPN) via simulation.NAT2TEST strategy dispense the need to know the syntax and semantics of the underlyingnotations, besides allowing early use of MBT, by means of Natural Language Processing (NLP).Nevertheless, the state explosion problem easily occurs in CSP version, therefore, our approachusing CPN simulation, where it is not necessary to explore its complete state space, minimisesthis problem.

1.2 Main contributions

The main contributions of this paper are the following:

� A systematic translation of DFRSs into CPN models, creating an alternative versionof the MBT strategy (NAT2TEST) for generating test cases using the formalism(CPN) via simulation;

� An improvement of the performance and detection of defects with respect to thestrategy via CSP;

We illustrate our overall approach with a running example.

3http://cpntools.org/

http://cpntools.org/

1.3. ORGANIZATION OF THE DISSERTATION 18

1.3 Organization of the dissertation

The remainder of this work has the following structure:

� Chapter 2 introduces the NAT2TEST strategy, Data-Flow Reactive Systems, ColouredPetri Nets, CPN Tools, and the Spoofax framework.

� Chapter 3 explains how to generate CPN models from DFRSs.

� Chapter 4 describes how to generate test vectors from CPN models via simulation.

� Chapter 5 presents an empirical analysis.

� Chapter 6 addresses our conclusions, related work and future directions.

191919

2Background

Here, we briefly introduce the concepts and tools used in this work. Section 2.1 presentsmore details about the NAT2TEST strategy and its constituent phases, in particular, its underlyingmodel DFRS (Section 2.2). Section 2.3 explains CPNs, the target formalism of this work, andbriefly describes the support tool for simulating CPN models by going through some of itsconstituent components. Finally, Section 2.4 describes the Spoofax framework, which is usedhere to develop a systematic translation from DFRSs to CPN models. As a running example,we consider a Vending Machine (VM), which is an adaptation of the coffee machine presentedin LARSEN K.; MIKUCIONIS (2004).

Runnig example From the initial state (idle), the VM goes to the choice state when it receivesa coin (REQ001). If the coffee request button is pressed, the state changes to the weak,provided the selection occurs within 30 seconds after inserting the coin (REQ002). Other-wise, the system changes to the strong state (REQ003). The time to produce a weak coffee(REQ004) is different from the time required to produce a strong one (REQ005). Afterproducing the coffee, the VM goes to the idle state.

As shown in Figure 2.1, in the VM example we have two input signals related to thecoin sensor (sensor) and the coffee request button (request). A true value means that a coin wasinserted and the coffee request button was pressed. There are two output signals related to thesystem mode (mode) and the vending machine output (output). The values communicated bythese signals reflect the system possible states (idle, choice, weak, strong, and reset) and thepossible outputs (undefined, weak, and strong).

The VM has just one timer: the request timer, which is used to register the moments whena coin is inserted, when the coffee request button is pressed, and when the coffee is produced.Figure 2.2 illustrates a scenario where there is continuous observation of the input and outputsignals. If we had chosen to observe the system discretely, we would have a similar scenario, butwith a discrete number of samples over time.

In Figure 2.2, a coin is inserted 2 seconds after starting the vending machine (the signalsensor changes to 1 —- true). Immediately, the system state changes from idle to choice. Here,

2.1. NAT2TEST STRATEGY 20

Figure 2.1: The VM abstract representation

the system states are encoded as follows: idle 7→ 1, choice 7→ 0, weak 7→ 3, strong 7→ 2, andreset 7→ 4. Therefore, this change is represented by changing the value of the signal mode from 1to 0. In this example, the signal sensor remains true for 3 seconds.

When 10 seconds have elapsed since the coin was inserted, which happens 2 secondsafter starting the vending machine, the user requests a coffee (the signal request becomes truewhen the system global clock is equal to 12). At this moment, the system state changes toweak coffee (the signal mode becomes 3). In this example, the signal request remains true for 4seconds.

As the coffee request occurs within 30 seconds of the coin being inserted, the systemproduces a weak coffee, which is represented as the value 2 of the signal output, 20 seconds afterreceiving the coffee request. We recall that a weak coffee is produced within 10 and 30 secondsafter the coffee request. Then, as stated by the requirements, the system goes to the reset state(the value of signal mode becomes 4), and 3 seconds later it goes back to the idle state, besidesresetting the output to undefined (the signal output becomes 1).

Figure 2.2: Example of VM signals

2.1 NAT2TEST strategy

In this section we briefly describe the NATural Language Requirements to TEST Cases(NAT2TEST) strategy for generating test cases from requirements written in natural language(CARVALHO et al., 2015). It is tailored to generate tests for Data-Flow Reactive Systems


(DFRS): a class of embedded systems whose inputs and outputs are always available as digitalsignals. In particular, regarding systems whose behaviour can be described by data operationsand that is time-dependent. The input signals can be seen as data provided by sensors, whereasthe output data are provided to system actuators.

It receives, as input, requirements (Example 2.1) written using the System RequirementsControlled Natural Language (SysReq-CNL), specially tailored for writing unambiguous re-quirements of data-flow reactive systems (CARVALHO, 2016). As output, it produces test cases.This test-generation strategy comprises a number of phases (see Figure 2.3). The three initialphases are fixed: (1) syntactic analysis, (2) semantic analysis, and (3) DFRS generation; theremaining phases depend on the target formalism from which test cases are generated. Somevariations have been explored (SCR (CARVALHO et al., 2014), IMR (CARVALHO et al., 2014)and CSP (CARVALHO; SAMPAIO; MOTA, 2013)). As already mentioned, we explore the useof CPN.

Example 2.1 This requirement (Vending Machine (VM)) adheres to the SysReq-CNL grammar.

� REQ002 – When the system mode is choice , and the coin sensor is false, and thecoin sensor was false, and the coffee request button changes to pressed, and the

request timer is lower than or equal to 30.0, the coffee machine system shall: reset

the request timer, assign preparing weak coffee to the system mode.

Figure 2.3: NAT2TEST strategy

The syntactic analysis phase receives as input the system requirements, and performs twotasks: it verifies whether these requirements are in accordance with the SysReq-CNL grammar,


Table 2.1: Example of a requirement frame for REQ002 (Vending Machine)

Condition 1 - Main Verb (CAC): isCPT: the system mode CFV: -CMD: - CTV: choiceCondition 2 - Main Verb (CAC): isCPT: the coin sensor CFV: -CMD: - CTV: falseCondition 3 - Main Verb (CAC): wasCPT: the coin sensor CFV: -CMD: - CTV: falseCondition 4 - Main Verb (CAC): changesCPT: the coffee request button CFV: -CMD: - CTV: pressedCondition 5 - Main Verb (CAC): isCPT: the request timer CFV: -CMD: lower than or equal to CTV: 30.0Action 1 - Main Verb (ACT): resetAGT: the coffee machine system TOV: -PAT: the request timerAction 2 - Main Verb (ACT): assignAGT: the coffee machine system TOV: preparing weak coffeePAT: the system mode

besides generating syntactic trees for each correctly edited requirement. The second phasemaps these syntax trees into an informal NL semantic representation, where thematic roles areidentified. As one can see in Table 2.1, the requirement frame (collection of thematic roles) ofthe example 2.1 contains five conditions and two actions. The roles that appear in actions are thefollowing: Action (ACT) — the action performed if the conditions are satisfied; Agent (AGT) —entity who performs the action; Patient (PAT) — entity who is affected by the action; and ToValue (TOV) — the patient value after action completion. In conditions, the roles are: ConditionAction (CAC) — the action that concerns each condition; Condition Patient (CPT) — the entityrelated to each condition; Condition From Value (CFV) — the CPT previous value; ConditionModifier (CMD) — a modifier related to the condition; and Condition To Value (CTV) — thevalue satisfying the condition.

The third phase (DFRS generation) derives an intermediate formal characterization of thesystem behaviour (s-DFRS) for the requirement frames. Other formal notations can be derivedform the DFRS. The possibility of exploring different formal notations allows analyses fromseveral perspectives, using different languages and tools, besides making the strategy extensible;as discussed previously, the target formalism in the present work is CPN, which is obtainedvia an systematic translation from DFRS. These first three phases are the same as the MBTstrategy NAT2TEST CARVALHO et al. (2015), and the NAT2TESTCPN can be considered as an

2.2. DATA-FLOW REACTIVE SYSTEMS 23

specialisation of the NAT2TEST framework.In the next phase (CPN generation), the s-DFRS is translated to the CPN model using

the Spoofax framework. This systematic translation involves defining an SDF3 grammar forDFRS models and transformation rules from DFRS to CPN. Finally, the test cases are generatedby simulating the CPN model via the CPN Tools. Table 2.2 shows part of a concrete test caseobtained from the previous requirement (REQ002).

Table 2.2: Example of test case for REQ002 (Vending Machine)

TIME request coin system mode output Trace0 false false idle strong18 false true choice strong REQ00156 false false choice strong72 true false preparing_weak_coffee strong REQ002

2.2 Data-flow reactive systems

A DFRS model (CARVALHO et al., 2014) provides a formal representation of therequirements semantics. It has a symbolic and an expanded representation. Briefly, the symbolicversion is a 6-tuple: (I, O, T, gcvar, sO, F). Inputs (I) and outputs (O) are system variables,whereas timers (T) are used to model temporal behaviour. These three sets (I, O and T) aredisjoint. There is a global clock denoted as gcvar. The element s0 is the initial state. The lastelement (F) represents a set of functions, each one describing the behaviour of one systemcomponent. The expanded DFRS comprises a (possibly infinite) set of states, and a transitionrelation between states. This expanded representation is built by applying the elements of Fto the initial state to define function transitions, but also letting the time evolve to define delaytransitions.

Table 2.3: The variables and types of DFRS for the VM example

Kind Name Type Expected Values Initial ValueINPUT the_coffee_request_button BOOLEAN {false, true} falseINPUT the_coin_sensor BOOLEAN {false, true} false

{choice, idle,OUTPUT the_system_mode INTEGER preparing strong coffee, choice

preparing_weak_coffee}OUTPUT the_coffee_machine_output INTEGER {strong, weak} strongTIMER the_request_timer INTEGER - 0

GLOBAL CLOCK gc INTEGER - 0

Tables 2.3 and 2.4 illustrate a DFRS for an adapted version of the Vending Machine (VM)(LARSEN K.; MIKUCIONIS, 2004). From the initial state (idle), it goes to the choice statewhen it receives a coin. If the coffee request button is pressed, the state changes to the weak

2.3. COLOURED PETRI NETS 24

Table 2.4: The functions of DFRS for the VM example

Static Guard Timed Guard Statements TraceFunctions: the_coffee_machine_system¬(prev(the_coin_sensor) = true) the_request_timer := gc, REQ001AND the_coin_sensor = true the_system_mode := 0AND the_system_mode = 1¬(prev(the_coffee_request_button)=true)AND the_coffee_request_button = true the_request_timer := gc, REQ002AND prev(the_coin_sensor) = false gc - the_request_timer30 the_system_mode := 2AND the_coin_sensor = falseAND the_system_mode = 0

state, provided the selection occurs within 30 seconds after inserting the coin. Otherwise,the system changes to the strong state. After producing the coffee, it goes to the idle state.In Table 2.4, one can note that the corresponding DFRS has two input (the_coin_sensor andthe_coffee_request_button) and two output (the_system_mode and the_coffee_machine_output)variables. The system behaviour is formalised by the function the_coffee_machine_system. Ithas five entries. Each entry comprises a 3-tuple: a static guard, a timed guard, and the expectedsystem reaction (a list of assignments).

2.3 Coloured Petri nets

Coloured Petri Nets (CPN) is a language for the modelling and validation of systemsin which concurrency, communication, and synchronisation play a major role. It is a discrete-event modelling language combining high-level Petri nets with an extension of the functionalprogramming language Standard ML (CPN ML).

CPN ML provides the primitives for the definition of data types, describing data manip-ulation, and for creating compact and parametrised models. A CPN model of a system is anexecutable model representing the states of the system and the events (transitions) that can causethe system to change state. The CPN language makes it possible to organise a model as a set ofmodules, and it includes a time concept for representing the time taken to execute events in themodelled system.

As described in (JENSEN, 1996), the formal definition of a CPN is given by a 9-tuple (Σ,P, T, A, N, C, G, E, I), satisfying the following properties:

� Σ is a finite set of non-empty colour sets (types).

� P is the finite set of all places.

� T is the finite set of all transitions.


� A is the finite set of all arcs such that P∩T = P∩A = T ∩A = /0

� N is the node function such that N : A→ P×T ∪T ×P

� C is the colour function such that C : P→ Σ

� G is the guard expression function such that G : T → Expr, and∀t ∈ T : [Type(G(t)) = Bool∧Type(Var(G(t)))⊆ Σ]

� E is the arc expression function such that E : A→ Expr, and∀a ∈ A : [Type(E(a)) =C(p(a))MS∧Type(Var(E(a)))⊆ Σ],where p(a) is the place of N(a);

� I is the initialization function such that I : P→ Expr, and∀p ∈ P : [Type(I(p)) =C(p)MS]

We denote by Expr the set of expressions provided by the inscription language (CPNML), and by Type(e) the type of an expression e ∈ Expr, i.e., the type of Var(e) (the valuesobtained when evaluating e). The subscript MS denotes the multiset of the associated place.

Informally, a CPN model describes both the states and the events of a system. Eventsare represented by transitions (drawn as rectangles) and the states are represented by places(drawn as ellipses or circles). These two kinds of nodes are connected by arcs that indicatethe direction in which tokens (data values) are moved. Arcs are used to connect places withtransitions, and vice-versa, but never two places or two transitions. Places hold collections oftokens, and thus represent local states (markings). The global state (or global marking) of amodel is represented by the distribution of tokens throughout its places. The places also have aninitial marking representing the initial local state. Figure 2.4 shows part of the CPN obtained forthe VM example (explained in the beginning of this chapter and illustrated in tables 2.3 and 2.4).In this illustration, we have part of the CPN that models the requirement REQ005—returning tothe idle state after producing coffee

As described in (TJELL, 2006), a transition (see the rectangle REQ005 in Figure 2.4)typically represents an event that occurs in the model. When this event occurs, the transition isenabled to fire. When a transition is enabled it means that it is ready to fire. When a transitionfires, it is able to remove tokens from its input places and to produce new tokens on its outputplaces, in a atomic action. The inscriptions in the arcs leading to a transition define the quantityof tokens needed for enabling the transition. Moreover, qualitative constraints can be specifiedfor the tokens from the input places. This can be done by the use of pattern matching or guardsin the transition.

A guard (see the text below REQx in Figure 2.4) is a predicate that must evaluate to truefor enabling the transition. For a given transition, if there is an available set of tokens from theinput places (in Figure 2.4 all places are input to the transition REQ005) while satisfying theseconstraints, this transition is enabled. If another transition also depends on some of the same


Figure 2.4: An example of a Coloured Petri Net (CPN)

tokens for being enabled, the transitions are said to be in conflict. This property is part of whatmakes (Coloured) Petri Nets a very strong tool for modelling distributed and concurrent systemswith shared resources, parallel processes and other characteristics that come with this type ofsystems.

In Figure 2.4, the first restriction to enable the transition REQ005 is that there are tokens inthe places Input, F_the_request_timer, F_the_system_mode, and F_the_coffee_machine_output.While there is some input to be processed, there will be tokens in Input. The remaining placeswill always have tokens because the tokens will ever be maintained or replaced by another whenthe transition REQ005 fires. The tokens in the place Input are only consumed when the transitionnoReq fires in the page NoAttendedReq. So, one can note that there is a bidirection arc fromthe place Input to the transition REQ005, unlike other places in the page REQ005. The otherrestriction is related to the guard condition that must be satisfied.

The graphical definition of CPNs is supplemented by declarations of functions, opera-tions, constants, variables, colour sets and priorities; all of them in the functional programminglanguage CPN ML (JENSEN; KRISTENSEN, 2009): an extension of the more commonlyknown Standard ML (MILNER; HARPER; TOFTE, 1990). Therefore, CPN models differ fromlow-level Petri Nets (such as Place/Transition Nets) by the fact that the tokens have types (coloursets) and values, and by the combination of programming languages.

The CPN modelling language also supports the specification of hierarchically structuredmodels as a collection of connected modules (or pages). This makes it possible to workwith different levels of abstraction, reuse of sub-modules in different parts of the model and

2.4. SPOOFAX FRAMEWORK 27

the construction of compact and parametrised models (JENSEN; KRISTENSEN, 2009). Amodule is itself a CPN model (possibly hierarchical too). Structuring is performed throughtwo mechanisms: fusion places or substitution transitions. Here, we use the former. A fusionplace is a set containing multiple places that may be found in different modules. Fusion setsare created for places that are repeated in more than one module (CPN page). This allowsinteraction to traverse boundaries of the modules in the model. For instance, in Figure 2.4, theplace Trace is contained in all pages of the VM model, except in Generator, and TestCase, so thefusion set Traces is associated to all the places Trace (see a thin rectangle at the bottom of thisplace in Figure 2.4). Other fusion sets that exist in this figure are Inputs, F_the_request_timer,F_the_system_mode, and F_the_coffee_machine_output.

CPN also allows the specification of time-based behaviour. This is accomplished byadding time stamps to tokens. In this way, delays are expressed as timing annotations in arcsand transitions. The firing of transitions is still an atomic event, but the calculation of enablingconditions for a given transition depends on the time stamps in the tokens it needs to consumethrough possible input arcs. Intuitively, the time stamp in a token can be seen as a specificationof the model time at which the token is available for consumption from a place.

CPN Tools1 is an industrial-strength computer tool suite for editing, simulation, statespace analysis, and performance analysis of untimed and timed, hierarchical Coloured Petri nets(CPN or CP-nets). Basic functions of CPN Tools consist in creation (editing) of model, analysisof models behaviour via its simulation, and creation and analysis of model’s state space (fulland partial). Using CPN Tools, it is possible to investigate the behaviour of the modelled systemusing simulation, to verify properties by means of state space methods and model checking,and to conduct simulation-based performance analysis. User interaction with CPN Tools isbased on direct manipulation of the graphical representation of the CPN model using interactiontechniques, such as tool palettes and marking menus.

The tool features incremental syntax checking and code generation, which take placewhile a net is being constructed. A fast simulator efficiently handles untimed and timed nets. Thestate space resource produces report containing information, such as boundedness and livenessproperties. The tool allows manual simulations or several replications.

2.4 Spoofax framework

Spoofax2 (KATS; VISSER, 2010) is a platform for the development of textual domain-specific languages. It is an Eclipse-based language workbench that uses the modular syntaxdefinition formalism SDF3, which supports language composition. Spoofax provides a compre-hensive environment that integrates syntax definition, program transformation, code generation,and declarative specification of IDE components. Actually, there are meta-languages for defining

1http://cpntools.org/2http://www.metaborg.org/en/latest/

http://www.metaborg.org/en/latest/http://cpntools.org/


languages in Spoofax: a syntax definition formalism (SDF3), a name binding language (NaBL),a type specification language (TS), and a transformation language (Stratego), as also the SpoofaxTesting Language (SPT). In what follows, we present an overview of the resources used in thiswork, based on (VISSER, 2015), where a more comprehensive explanation is provided.

The SDF language describes a grammar, an algebraic signature, and a mapping fromparse trees to abstract syntax trees at once. Indeed, from just an SDF3 syntax definition, onecan generate the abstract syntax signature, error recovery rules, a parser, a mapping from parsetrees to abstract syntax trees, a pretty-printer (mapping from abstract syntax trees to text), syntaxhighlighting rules, and folding rules. Therefore, an SDF3 definition is a declarative, integrated,and modular description of all aspects of the syntax of a language, including its lexical syntax.

Using the high-level SDF grammar formalism, one can write the language grammar.Based on this grammar, basic editor services such as syntax highlighting and code folding areautomatically provided. Using high-level descriptor languages, these services can be customised.More sophisticated services such as error marking and content completion can be specified usingrewrite rules in the Stratego language. In Example 2.2, it is defined a SDF3 grammar for aDomain-Specific Language (DSL), whose programs in that language have a name, then define alist of zero or more classes, and finally an expression to be executed in the context of these classdefinitions. The module imports the syntax of Classes and Expressions and defines a context-freesyntax production to define the syntax of programs.

Example 2.2 A short example of an SDF3 definition (VISSER, 2015).

module ProgramsPlainimports Classes Expressionssorts Program

context-free syntaxProgram.Program = [program [ID] [Class*] run [Expr]]

An SDF3 definition defines both the concrete syntax and abstract syntax views of alanguage. The following is a minimal program in the concrete syntax of the language thatexecutes the expression 1 in the context of no classes:

program program01 run 1

Here is the same program in abstract syntax representation:

Program("program01", [], Num("1"))

Thus, the Program production is equivalent to the context-free grammar production:

Program = "program" Class* "run" Expr

defining the concrete syntax notation of programs. By the way, the * in Class* is the Kleene-starand denotes a sequence of zero or more strings matching the Class non-terminal sort.


The Stratego language provides rewriting rules for expressing basic transformations,programmable rewriting strategies for controlling the application of rules, concrete syntax forexpressing the patterns of rules in the syntax of the object language, and dynamic rewrite rules forexpressing context-sensitive transformations, thus supporting the development of transformationcomponents at a high level of abstraction. In Example 2.3, the rule to-xml translates a programfrom the language defined above to XML format by exploring the abstract tree. The abstractterm Program is decomposed via string interpolation into the XML tags. The stratego librarydefines the dbg(|msg) strategy, which prints the current term prefixed with msg, and the strategymap(s), which applies s to all the elements of a list (cs). The strategy combinator $[

[

303030

3Translating from DFRS to CPN

In this chapter we explain how DFRSs, encoded as eXtensible Markup Language (XML)files, are systematically translated to CPN models, in accordance to the CPN format accepted byCPN tools. In Section 3.1 we explain how DFRSs are represented as CPN models. Afterwards,in Section 3.2 we describe how to perform this translation in a systematic way: first, proposing agrammar for DFRSs (Section 3.2.1), then defining translation rules in Spoofax (Section 3.2.2).

3.1 CPN models

Intuitively, the behaviour of a DFRS is encoded as transitions that modify the correspond-ing output variables, which are modelled as CPN places (see Section 2.3). Therefore, the targetof these transitions are the output places, and their source are auxiliary places that provide to thetransitions the system inputs, along with the output and timer places. The generation of CPNmodels from DFRSs is accomplished in three steps, as explained below.

So, for representing a DFRS as a CPN model, firstly DFRS input variables, and theirtypes, are translated to CPN variables and colour sets (Section 3.1.1), respectively. In thefollowing step, DFRS output variables are mapped to places along with the corresponding colourset (Section 3.1.2). Finally, the DFRS functions are represented in the CPN model as transitions(Section 3.1.3). In what follows, we detail these steps. To illustrate the relevant concepts, in thenext sections, we consider the adapted VM example briefly described in Section 2.2.

3.1.1 Representing input variables

By definition, the DFRS functions (requirements) do not change the DFRS input states;therefore, it is not necessary to represent each one of them through CPN places, which wouldincrease the complexity of the model. Hence, just one place (Input) is created to store all thevalues generated for the input variables. For each input variable of the DFRS, two CPN variablesare defined along with the corresponding colour set (type). These two variables store the previousand current values (used by the transition guards when the respective requirement containsthe verb becomes or changes) for each entry. For a DFRS variable named the_coin_sensor,we generate the variables pthe_coin_sensor and the_coin_sensor, to stand for its previous and

3.1. CPN MODELS 31

Figure 3.1: Page created to represent the requirement REQ001

the current value, respectively. These mentioned CPN variables are used to transmit the inputvalues (tokens) to the transitions during the simulations. The place Input is created in the pageGenerator (see Figure 4.1), in the page NoAttendedReq (see Figure 4.2) and in all the pages thatmodel the DFRS functions (see Figure 3.1). These places are linked by a fusion set (see the labelInputs in the just mentioned figures). The type (INPUTLIM) in the place Input comprises aninteger value (to limite the number of input values being randomly generated) and the types ofthe input variables (repeat twice for each input variable).

3.1.2 Representing output variables

In this case of output variables, as DFRS functions (requirements) can change DFRSoutput states, they are represented by places (to store states), variables (to transmit the previousand current values), and a colour set equivalent to their type. In contrast with the input variables,the output variables do not store a DFRS state, they just transmit or change the state store in theplace marking (see the variables the_system_mode and the_coffee_machine_output in Figure 3.1).When a transition that modifies an output is fired, it leads the tokens to the respective placechanging its marking and, thus, the value of the corresponding CPN variables accordingly. Eachone of these places has as initial marking the initial value of the corresponding DFRS outputvariable.

Considering the VM example, we have two DFRS output variables that represent thesystem mode and the coffee machine output. The system mode has four possible modes: choice,idle, preparing strong coffee and preparing weak coffee. The coffee machine output has two

3.1. CPN MODELS 32

possible values: strong and weak. As previously said, for each DFRS output variable, we createa place (the system mode and the coffee machine output), a variable (the_system_mode andthe_coffee_machine_output), and a colour set (OCSTHE_SYSTEM_MODE1 – an enumerationcomprising the four aforementioned values, and OCSTHE_COFFEE_MACHINE_OUTPUT –other enumeration comprising the two values, previously listed). When the transition REQ001 isfired (see Figure 3.1), the marking of the place the system mode is changed from idle to choice. Asexplained in Section 2.3, CPN transitions are created to represent the system requirements. Thearc leading to the place the system mode has as inscription choice, since the requirement REQ001describes the situation when the system mode becomes choice. Note that this requirement doesnot cause any change in the variable the_coffee_machine_output, so both arcs have the sameinscription. Also, note that the page NoAttendedReq produces no change in the places thatrepresent the DFRS outputs (see Figure 4.2).

3.1.3 Representing functions

For each function of the DFRS (a system requirement), a page is created to representthe function behaviour, thus simplifying individual behaviour analysis of system requirements.Therefore, one CPN page is created to model each function entry. For easing traceability ofCPN pages to the requirements, the page is named according to the requirement related to theconsidered entry.

Each requirement page comprises some places and one transition. The transition (namedafter the requirement identifier) represents a possible system reaction – models how the outputvariables must be updated. Therefore, this transition has outgoing arcs to one or more places (theones that represent DFRS output variables) whose marks must be modified when the transition isfired. Besides the places that represent DFRS output variables, there are two other places (Inputand Trace) that are auxiliary elements (later explained in Section 4.1).

Regarding DFRS models, the functions represent the system actions arising from therequirements. Therefore, as explained in Section 2.3, they are translated into transitions within aCPN model. These transitions have guards (conditions to be enabled), which denote a conjunctionof the static and timed guards of the DFRS. The ingoing arcs inscriptions of these transitionstransmit the values of the input and output DFRS variables, which are used by the guardsand by the output arcs of these transitions. Considering the requirement REQ001 of the VMexample, and the corresponding function entry (REQ001 line in Table 2.4), we create the arcsthe_system_mode and the_coffee_machine_output (see Figure 4.1). As one can see, these arcsare guarded by the conjunction of the corresponding static and timed guards. (see Figure 3.1).

To give a concrete example, consider the adapted VM and the function entry relatedto REQ001 (see Table 2.4): (¬(prev(the_coin_sensor) = true)∧ the_coin_sensor = true∧the_system_mode = 1). It means that when the system mode is 1 (idle), and the coin sensorchanges to true, the coffee machine system shall change the system mode to 0 (choice) and reset

1Output Colour Set (OCS)

3.2. SYSTEMATIC TRANSLATION 33

the request timer (assigns the global clock value to the timer).For modeling this function entry, the page REQ001 is created, along with the transition

REQ001. To enable this transition, the associated guard needs to evaluate to true. This guard([not(p_the_coin_sensor = true) andalso the_coin_sensor = true andalso the_system_mode =idle, not(the_system_mode = choice)]) is a translation of the guards of the correspondingfunction entry. The variable p_the_coin_sensor stands for the previous value of the coin sensor.The last restriction of this guard (not(the_system_mode = choice)) is required to ensure thistransition just becomes enabled when a state change will occur as a consequence of firing thistransition (later explained in Section 4.2.2).

Besides satisfying its guard, the transition also needs to know the current and previousvalues of the system inputs, along with the value of the system outputs. Note that the afore-mentioned guard also depends upon the value of a system output – the system mode. Thesevalues (tokens) are sent to the transition REQ001 by the arcs emanating from the places Inputand the system mode. When this guard evaluates to true, and the required tokens are available,the transition fires and assigns choice to the place the system mode. As previously said, for everyentry of each DFRS function, a page similar to this one is created.

3.2 Systematic translation

In this section we describe the approach used to translate from DFRS to CPN modelin a systematic way: first, proposing a grammar for DFRSs (Section 3.2.1), then definingtransformation rules in Spoofax (Section 3.2.2).

3.2.1 Defining a DFRS grammar

As explained in Section 2.2, a DFRS model, an intermediate formalism describing thesystem behaviour, is composed by three disjoint sets of input and output variables, as well asinternal timers. It also has a global clock. The system behaviour is represented by functions,each on with a pair of guards, along with its corresponding reaction, represented by assignments.

The system needs to have at least one input and one output variable; however, there maybe no timers, when the system has no temporal aspects. For each variable it is known its name,its type (boolean, integer or float), and its initial value. The global clock is always named gc.When translating to CPNs, to enable simulation (see Section 4.1.1), we also need to have a list ofvalues to be considered during simulation. This information is required only for input variableswhose type is integer. For variables of enumerated types we can consider all the possible values,as these are necessarily finite.

A function, which describes the system reaction in a given context, is defined by anon-empty set of tuples. Each tuple is composed by a name, and a pair of static and timedguards (boolean expressions), and a set of assignments that shall be performed when both guardsevaluate to true. The static guards shall refer to input and output variables, whereas the timed


Figure 3.2: Part of the XML representation of the DFRS for the VM example

guards are restricted to expressions over timers. One of the guards can be empty, but not both.Besides the aforementioned information, the NAT2TEST tool also keeps traceability information(the identifier of the requirement that is the source of the corresponding tuple). See a part of theXML representation of the DFRS for the Vending Machine (VM) example in Figure 3.2.

To define a systematic translation from DFRSs to CPNs, we first need to define agrammar, which, concretely, we adopt an XML representation of DFRS models; so far, thesemodels were only held in memory. In the XML grammar for DFRS models (Figure 3.3), one cannote that the input (INVar) and output (OUTVar) variables have the same definition, except fortheir XML tags. The Timer (TimerDef ) and Global Clock (GClock) definitions are also similar;however, the global clock name is the constant gc. A function can have one or more tuples(FuncTuple). Each tuple comprises a pair of static (SGuard) and time (TGuard)) guards, thecorresponding assignments (Stm+), besides the requirement ID for traceability purposes (Req).Each assignment is composed by a variable identifier (VarName) and a value to be assigned(Expression).


Figure 3.3: DFRS grammar

3.2.2 Creating transformation rules

The translation from DFRSs to CPNs occurs via transformation rules2, which are dividedinto modules for easy understanding and maintenance. In this work, they were structured inmodules according to the XML format for .cpn files, that is, the order they should be presentedin a CPN file. (See the Document Type Definition (DTD) for .cpn files in Appendix B)

The first section of the CPN file is the globbox, which is divided into two blocks:Standard priorities (for the transitions) and Standard declarations (wherein are declared theconstants, variables, coloursets, functions and operations of the CPN). Therefore, the modulecpnDeclarations is created for defining the transformation rules for these blocks. For instance,the rule create-cpn-inputs (Figure 3.4) creates the declaration of input variables, where thecurrent and previous values for each given input of the DFRS are stored. Note that the rule inputis the abstract term INVar, obtained from the generated Abstract Syntax Tree (AST) accordingto the DSL proposed here, and it generates as output the variable declarations contained in thisterm (INVar). The rule create-colorset-input provides the type (colorset) of these input variables.

Afterwards, the modules for creating CPN pages are specified. The module pgGeneratorcontains the rules that create the page Generator, which generates the system input values and

2Available for download at: https://github.com/NatCPN/TransformRules

https://github.com/NatCPN/TransformRules


Figure 3.4: The rule create-cpn-inputs

comprises a place to store all of them, a place to limit the quantity of input vectors and thetransition to generate the random system entries, along with their respective arcs. Most of thispage contains fixed components that do not depend on the modelled system. The variable partconsists only by the vector of the initial input values, the vector of the generated values for theentries, the vector of the input variable names and a setting for working with continuous ordiscrete time, as appropriate. The transformation rule round-tistamp (see Code 3.1) performsthis configuration. From the term Timer (line 2), the aforementioned rule defines whether themodel will work with continuous or discrete time. When the timer type (vt) is Integer (line 5),the model timestamps are rounded by the operator round (line 6).

Code 3.1: Stratego – The transformation rule round-tistamp1 round−t i s t a m p :2 Timer ( TimerDef ( VarName ( vn ) , v t , I n i t i a l V a l u e ( i v ) ) ) −> cs3 where4 s w i t c h ! v t5 c a s e ! v t => I n t e g e r ( ) :6 cs := $ [ round ]7 o t h e r w i s e :8 cs := $ [ + ]9 end

The pgNoAttReq module specifies the rules that create the page NoAttendedReq (men-tioned in Section 3.1.2), which deals with the situation when no different system reaction isobserved. This page contains a unique transition, with low priority, which is enabled only in asituation where no system requirement (DFRS function) is satisfied. In this case, the input isconsumed, being transmitted from the Input place to the Test Oracles place. The Input placeis a clone of the place with the same name in the Generator page, which stores the entries


Figure 3.5: The rule page-reqx

generated for the simulation model. The place Test Oracles stores the test vectors to be writtento a Comma-separated values (CSV) file. This page also has fixed and variable portions.

The pgReqX module contains the rules that generate the requirement pages, which modelthe DFRS functions (see example in Figure 3.1). These pages are similar to the pgNoAttReqpage with respect to its components; however, it does not have the Next TO and Test Oraclesplaces. As in the previous page, rules are created for generating places for each of the outputvariables and timers. Note in the Figure 3.5 that the page-reqx rule organizes the terms of thesyntax tree so that a page is created for each system requirement. Then the page-reqx-body rulecalls the rules: place-input-reqx (to create the Input place), reqx-trans (to create the transitionassociated to the corresponding requirement), reqx-vo-places (to create places that model DFRSoutputs) and reqx-ti-places (to create places that model the timers).

The pgTestCase module contains the rules that create the TestCase page, responsiblefor processing the generated test vectors, that are stored in a CSV file. In this module, rules arecreated for deriving the names of the input and output variables, as well as their initial values.

The cpn-options module creates a special section of the cpn file containing: fusions (foreach place that is repeated on different pages), instances (one for each CPN page required) andsome settings (options) of the Coloured Petri Nets (CPN). The only option we need to handle isthe realtimestamp, to specify whether the CPN model will handle continuous or discrete time,which depends on the system being modelled.

It is worth mentioning that a lot of information, such as size, shape and position of thefigure representing the transitions or places, as well as the colours were defined from trials andare not relevant for generating test cases, but only for visual inspection of the models.

383838

4Test vectors based on CPN simulation

In order to generate test cases via CPN simulation, it is necessary to complement themodel generated in Section 3.1 with some auxiliary elements (Section 4.1). Section 4.2 presentshow test vectors are generated via simulation of a CPN.

4.1 Auxiliary components

After constructing a CPN model to represent a DFRS (Section 3.1), via the translationmentioned in Chapter 3, we now create auxiliary components, which are used to stimulate themodel and to generate test cases. These components (places, transitions, and arcs) are always thesame, but parametrised by the number of inputs and outputs. Considering the constant InputQty,which is defined beforehand to limit the number of generated inputs, the following auxiliaryelements are created: Generator, NoAttendedReq, TestCase.

4.1.1 Generating entries

A page (Generator) is created to generate input values randomly (Figure 4.1). Whenfired, the transition Generate Inputs produces the system inputs, and transmits them, along withan index i, to the place Input. This index is used to ensure the order the generated inputs areconsumed by the transitions that represent the system behaviour. This index is initially 0 (see thefirst element of the place Input’s initial marking). We note that the generated inputs are also aninput to the transition Generate Inputs. It is necessary because when generating the next inputs,the token sent to the place Inputs might comprise the newly generated values (TYPE.ran()), butalso the previous values of the inputs. When the number of generated inputs reaches InputQty,the transition Generate Inputs becomes disabled. The place Next Input aids this control. At thismoment, no more inputs (tokens) are generated by this transition. The place Input is initialisedby the initial values of the DFRS input variables. The aux text (CPN’Replications.nreplicationsInputQty) is used to perform a predefined quantity of simulation.

4.1. AUXILIARY COMPONENTS 39

Figure 4.1: Page created to generate the inputs randomly

4.1.2 Dealing with no system reaction

A page (NoAttendedReq) similar to those that represent the requirements (DFRS func-tions) is created. Although this page has a transition (noReq) that consumes the inputs (tokensin the place Input), this transition, unlike those in the pages that model requirement functions,does not change the value of the places that represent output variables (see in Figure 4.2 thebidirectional arcs pointing to the places the_system_mode and the_coffee_machine_output). Thistransition is enabled when no other transition is enabled, and it represents the idea that when nosystem reaction is expected for a given input, the system does not change its outputs (their valuesremain the same). To ensure that noReq is only enabled when no other transition is enabled, ithas a lower priority (P LOW).

The place Next TO is used to order the obtained test vectors. When the transition noReqfires, it produces a token that represents a test vector: the received inputs, along with the expectedoutput values. As one can see in Figure 4.2, this token begins with an index z, and the expressiontime(). This index, which is controlled by Next TO, establishes an order for the tokens stored inTest Oracles. The expression time() is used to get the time from the global clock in which the testvector is generated. Another element of this tuple is the label trace to track which requirementsproduced the output. This label allows us to relate generated test vectors with requirements and,thus, extract coverage information with respect to the system requirements. The place Tracestores the label transmitted by the transitions that represent the requirements.

4.1. AUXILIARY COMPONENTS 40

Figure 4.2: Page created to deal with no system reaction

4.1.3 Creating a test case file

As one can see in Figure 4.3, the page TestCase stores the steps (test vectors) of thegenerated test cases in a CSV file. The transition Write File that manipulates the CSV files isenabled when all inputs are generated, that is, when the index i (received from Next Input) isequal to the defined number of the test case inputs (InputQty). The created test vectors, whichare stored in the place Test Oracles and ordered by the index z, are written in the CSV file whenthe transition fires.

This transition executes the associated code segment (see Code 4.1) to create a CSV filein the output simulation path. First, when the transition receives the first tuple whose variable rtis equal to 0, it initialises a file (TC.csv), and adds to it a header – the name of the columns, whichare named after the system input and output variables (lines 1 – 3). Afterwards, it appends to thisfile a test vector every time the transition Write File is fired (lines 6 – 8). When all generatedoutputs are processed from the place Test Oracles, and it has only the tuple whose label req isSTOP, the transition fires closing the file previously created (line 9).

Code 4.1: Action of the transition Write File code segment1 i f r t =0 t h e n ( o u t f i l e := TextIO . openOut (OS . Pa th . c o n c a t2 ( Outpu t . g e t S i m O u t p u t D i r ( ) , "TC . csv " ) ) ;3 TextIO . o u t p u t ( ! o u t f i l e , Head ) ) e l s e ( )4 i f r t >=0 t h e n5 i f r e q "STOP" t h e n6 TextIO . o u t p u t ( ! o u t f i l e , v e c t o r ( r t , t h e _ c o f f e e _ r e q u e s t _ b u t t o n ,7 t h e _ c o i n _ s e n s o r , the_system_mode ,

4.2. TEST VECTORS GENERATION 41

8 t h e _ c o f f e e _ m a c h i n e _ o u t p u t , r e q ) )9 e l s e ( TextIO . c l o s e O u t ( ! o u t f i l e ) ) e l s e ( ) ;

Figure 4.3: Page created to save the test cases in a CSV file

4.1.4 Repeated places

Fusion sets are created to aggregate places replicated throughout the model pages, that is,all of them represent the same place. For instance, the place Input is an element of all pages,except for TestCase; so, the fusion set Inputs is associated to all the places Input (see a thinrectangle at the bottom of these places in Figures 3.1, 4.1 and 4.2). The same occurs to theplaces Test Oracles, to which the fusion set Tests is created, and comprises the places replicatedin the pages NoAttendedReq and TestCase (Figures 4.2 and 4.3, respectively). Other fusion setsare NextInput (in the pages Generator and TestCase), and Traces (in the pages NoAttendedReqand those that represent the system behaviour). Finally, fusion sets are created to aggregateall places that represent the DFRS output variables or the DFRS timers (see examples of thesefusion sets in Figure 4.2).

4.2 Test vectors generation

Once the CPN model is generated, as previously explained in Chapter 3 and Section 4.1,it is possible to generate test cases automatically via CPN simulation: it randomly producesinputs, along with the expected outputs. The tool (CPN Tools) has a number of resources torun simulations; for instance, it can be performed with user intervention or automatically, it canalso be repeated n times (simulation replications). Besides generating test cases, simulations


Figure 4.4: Page created to represent the requirement REQ002

can be used to validate the system requirements. The proposed model is constructed so that thesimulation takes place in three steps: generating random inputs, processing the inputs by thetransitions obtained from the system requirements (or by the transition noREQ), and recordingthe test case file. These steps are detailed below.

4.2.1 Random inputs generation

When the simulation starts (time 0), the transition Generate Inputs fires and an inputis randomly produced using the ran function. As the initial values are considered to be thosedefined in the DFRS, they are reflected as the initial marking of the place Input. The number ofinputs is initially preset as the value of the constant InputQty. Once the type of the place Input istimed, the generated tokens (representing the inputs values) are sorted by a timestamp.

Considering the VM example, Figure 4.5 shows two tokens in the place Input marking(the first token – (0, f alse, f alse, f alse, f alse)@0, is an initial marking, and another one –(1, f alse, f alse, f alse, true)@11, a randomly generated value). The first token timestamp is@0 and the generated one is @11. Also at time 0, the next enabled transition that fires isnoREQ, processing the initial input, whose timestamp is @0. As one can see in Figure 4.6,now the place Input has only one token, and the place Test Oracles contains a new token –(1,0, f alse, f alse, idle,strong,””)@0, produced by the transition noREQ firing, along with theTest Oracles initial marking – (18,9999, f alse, f alse, idle,strong,”STOP”)@0.


Figure 4.5: Generating random inputs

4.2.2 System reaction

In the next step, for each input, the model verifies whether there is at least one enabledtransition. When a transition that represents the system behaviour is fired, the places that modelthe DFRS outputs and timers are updated according to the expected system reaction, and a labelis appended to the place Trace marking. When the fired transition is noREQ, it produces as outputa tuple. The produced tuple comprises: an ordering index, a processing time, the current valuesof the inputs and outputs, and a label to track which requirements produced the output. Theoutputs are sorted with the support of the place Next TO. If for a given input there is no expectedsystem reaction, the transition defined in the page NoAttendedReq is fired. It produces as outputa new tuple keeping the output values the same. Considering the VM example, Figure 4.6 showstwo test vectors stored in Test Oracles via CPN simulation.

4.2.3 Test vectors

Finally, in the last phase, the transition Write File records the test cases in a CSV file. Toaccomplish this task, a code segment is used (shown in Code 4.1), which is executed when thistransition fires. The place Next Output is used to keep the outputs ordering.

In the CSV file, the generated test vectors are shown in a tabular form (Table 4.1).Considering the VM example, the first column (T IME) is the input timestamp previouslyexplained. The next columns list the system inputs, as well as the corresponding expectedoutputs. The last column provides traceability information between the expected system reactionwith the system requirements. This latter column is empty when it refers to a test vector that wasgenerated by firing the transition noREQ.


Figure 4.6: Processing the initial input by the transition noREQ

The test case presented in Table 4.1 describes the following scenario. Initially (time 0),all inputs are f alse, that is, there is no coin in the machine, and the request button is not pressed.The system mode is idle, and the coffee machine output is the preset value strong. When a coinis detected by the coin sensor (time 18), the system mode changes from idle to choice (accordingto the requirement REQ001). Afterwards, there is no transition associated to a requirement thatcan fire, and thus, the transition noReq fires transmitting the test vector to the place Test Oracles(see Figure 4.6).

Therefore, as one can see, the test generation approach proposed here behaves accordingto the following cyclic pattern: first, it performs as many transitions related to requirements aspossible; when none of these transitions are enabled, it performs the noREQ transition; finally, itreceives new inputs.


Table 4.1: Example of a test case for the adapted Vending Machine(VM)

TIME request coin system mode output Traceability0 false false idle strong

18 false true choice strong REQ00156 false false choice strong72 true false preparing_weak_coffee strong REQ00299 false false idle weak REQ004

142 true true choice weak REQ001173 true false choice weak205 false true choice weak221 true true choice weak254 true false choice weak277 true false choice weak291 true false choice weak301 false true choice weak322 true true choice weak345 false true choice weak377 true false preparing_strong_coffee weak REQ003419 false false idle strong REQ005

464646

5Empirical analysis

Here, we discuss how our strategy, a specialisation of the NAT2TEST that considersColoured Petri Nets (CPN), was evaluated considering examples from the literature and theaerospace industry. In order to allow for a comparison with the empirical results obtained whenevaluating the NAT2TESTCSP strategy, we follow here the same steps and guidelines consid-ered in (CARVALHO, 2016). For each domain, we analyse two aspects: (i) the performance(Section 5.1) of the NAT2TESTCSP and NAT2TESTCPN strategies; and (ii) the ability to detectdefects by means of mutation analysis (Section 5.2). As a baseline we considered the generationand execution of random tests using Randoop (PACHECO et al., 2007). It is important to bear inmind that threats to validity apply to this work, as listed below.

� Conclusion validity: design decisions considered when creating the reference Javaprograms might influence the results obtained, in particular, the ability of detectingerrors via random testing. Moreover, the conclusions were not drawn with the aid ofstatistical analyses due to the few examples considered.

� Construct validity: our analysis regarding the ability to detect defects consideredmutation analysis of Java programs, and random testing as baseline. Considering thenature of the domain of this work (timed reactive systems), it would be better to haveconsidered embedded software instead of Java code.

� External validity: as we considered few examples, and they are of relatively smallsize, we cannot statistically generalise the reached conclusions.

Despite that, the results allow interesting insights and provide some evidence about thefeasibility of our proposal.

5.1 Performance analysis

For all time measurements, we use an i5-3317U CPU with 1.70GHz equipped with 6GB of RAM memory running the Windows 8.1 operating system. Table 5.1 presents the metrics

5.1. PERFORMANCE ANALYSIS 47

Table 5.1: Perfomance Analysis

NAT2TESTVM NPP PC

# of requirements/words: 5/232 11/268 8/294Time to process the reqs.: 0.11s 0.07s 0.14s# of cond./actions/TRs: 18/10/130 21/11/149 26/8/162Time to identify the RFs: 0.10s 0.14s 0.10s# of I/O/T: 2/2/1 3/3/0 4/1/0Time to generate the s-DFRS: 0.02s 0.01s 0.01s

NAT2TESTCSPTime to generate the CSP: 0.04s 0.02s 0.01s# of concrete test cases: 25 55 30Time to create tests (FDR2/Z3): 94.87s/1.19s 39.23s/0.90s 4.52s/0.47sTime to run the tests: 11.03s 4.49s 0.98s

NAT2TESTCPNTime to generate the CPN: 0.14s 0.34s 0.13s# of concrete test cases: 32 36 25Time to create the tests: 0.34s 1.61s 0.94sTime to run the tests: 23.22s 2.75s 0.69sCPN - total time: 23.70s 4.70s 1.76s

Randoop# of test cases: 100 100 100Time to create the tests: 3.18s 1.80s 3.15sTime to run the tests: 73.35s 76.20s 29.05sRandoop - total time: 76.53s 78.00s 32.20s

related to our performance analysis. Multiple runs were performed and we consider the averagetime.

The three examples (see the complete list of requirements in Appendix A) comprisesystems with 2 (VM) to 4 (PC) inputs, and with 2 (VM) to 3 (NPP) outputs. As one can notethe examples NPP and PC do not have timers, that is, they do not have timed-based behaviour.Therefore, no timers are required in these examples.

Both strategies NAT2TESTCSP and NAT2TESTCPN share the first three phases (syntacticanalysis, semantic analysis and generation of DFRS). As it can be seen in Table 5.1, the timerequired to perform these steps are not significant (less than 300ms, on a Linux operating system).The most time-consuming step in the NAT2TESTCSP strategy is the generation of test cases(approximately VM: 95s, NPP: 40s, and PC: 5s), since this is performed via refinement checkingand SMT solving, using the FDR2 and the Z3 tools, respectively (for further details, we referto (CARVALHO, 2016)). Differently, when considering CPN models, this step is significantlyfaster (see Table 5.1). The underlying reason is that when simulating a CPN model, it is notnecessary to explore the model complete state space, what is required when generating test casesusing FDR2/Z3.

5.2. MUTANT-BASED STRENGTH ANALYSIS 48

It is important to highlight that the metrics concerning the NAT2TESTCSP strategy weremeasured in a different environment (operating system and computer), since it is Linux-based,whereas the NAT2TESTCPN strategy is Windows-based. Nevertheless, even if considering thesame environment, the CPN-based version tends to be faster than the version using FDR2/Z3 dueto the reason explained before (time required to perform simulations versus refinement checkingand SMT solving).

The automatically generated test cases were used to find faults systematically createdby code mutation in Java programs (see Section 5.2). In the strategy using CSP, within 11.03s,4.49s, and 0.98s the complete set of tests were ran against all mutants generated from the VM(283), NPP (319), PC (134), respectively. In the NAT2TESTCPN strategy the set of tests were ranwithin 23.22s 2.75s 0.69s, respectively. In the NPP and PC examples the CPN strategy scaledbetter, but when the example (VM) has timed behaviour, the performance was worse.

Similar to (CARVALHO, 2016), to provide a baseline, we used Randoop to randomlygenerate test cases from the same Java programs created for each analysed example. In theseexperiments we were able to handle only a relatively small set of random test cases. The reasonis not the time required to generate these tests (Table 5.1 shows that the tests were generatedwithin 4s), but the amount of memory needed to run these random tests. With more test cases,we got a Java OutOfMemory exception concerning the Java PermGen space. Each randomtest created by Randoop instantiates a Java object. With this object, Randoop performs severalrandom manipulations, and finally asserts its state to check whether it is equal to the expectedone. Hence, a huge number of objects are created within a short amount of time, and the Javagarbage collector does not handle them as fast. The total time required by the NAT2TESTCPNstrategy, for each example, is significantly smaller than the Randoop time.

5.2 Mutant-based strength analysis

A mutant-based strength analysis was performed to assess the quality of the tests gener-ated by the NAT2TESTCPN strategy. The same environment of the time measurements are usedfor the mutant-based strength analysis. Below, we explain the employed approach.

To compare the test cases strength, we use mutation operators that create erroneousprograms in a controlled and systematic way. Thus, a good test case should be able to detect theintroduced error (i.e., kill the mutant). Sometimes the alive mutant is equivalent to the correctprogram. However, in general, such a verification is undecidable and too error-prone to be mademanually.

In this work we adopted the same strategy of (CARVALHO, 2016), i.e, we assume thatall alive mutants are considered different. In other words, if some alive mutants are semanticallyequivalent to the original program, which might happen, the resulting mutation score would behigher as these mutants would not be considered. Therefore, the results presented here consist ofa worst-case analysis.

To perform the mutant-based strength analysis reported

Documents

CPN SIMULATION-BASED TEST CASE GENERATION ......A utilização de testes baseados em modelos (MBT) apresenta-se como alternativa para solução destes problemas, através do uso de