WIXLIB

4Prefacerequirements analysis, their modeling and “translation” of high-level requirements presentedto the level of implementation under test interfaces.– The second problem is the issue of how to obtain “good” models. It is both technical (in whatform models should be designed) and organizational (how to build a joint process of implementation design and model design). The experience shows that skilled software designersdon’t want to duplicate their work and waste time on designing a model, besides the implementation itself; and unskilled programmers can do well neither in coding nor in behaviormodeling. MBT deployment requires substantial resources, however there are no fundamental difficulties ifthe organization decides to introduce MBT in practice. A good example to this is the experienceof Microsoft lab in China (see for instance W. Grieskamp, Xiao Qu, Xiangjun Wei, N. Kicillof, M.B. Cohen. Interaction Coverage meets Path Coverage by SMT Constraint Solving [5]). MBT is actively used in the fields having the experience of systematic certification of softwaresystems, particularly in avionics and automotive. Since this domain is becoming more and moreimportant, a challenge is to align MBT with certification processes and regulations.This year’s MBT workshop features Ana Cavalli from Institut National des Telecommunications,Paris, France as invited speaker. In her speech, entitled “Evolution of testing techniques: from activetesting to monitoring techniques”, she presents the evolution of these testing techniques, their advantagesand limitations, and illustrates the application of monitoring techniques to the security testing of real casestudies.The contributions selected by the Program Committee reflect both applications of MBT in industrialpractice and further development of MBT theory and techniques.Ana Rosario Espada, Maria Del Mar Gallardo, Alberto Salmerón and Pedro Merino present an approach to automated model construction and test generation for Android mobile applications. MarcusGerhold and Mariëlle Stoelinga extend the well-known notion of input-output conformance to probabilistic state machines, opening the door to development of new classes of models and test constructiontechniques. Paul Jorgensen presents a novel variation of Petri-nets to facilitate visual modeling of interacting components in complex systems. Hartmut Lackner and Martin Schmidt discuss quality of testsuites for product lines and develop an assessment approach based on mutation operators applied to software product lines. Natalia Kushik and Nina Yevtushenko present new result in the theory of FSM; theyshow that for some FSMs its homing sequence can be built in polynomial time.The workshop is concluded by a remotely presented talk by Yury Gurevich on “Testing Philosophy”.We would like to thank the program committee members and all reviewers for their work in evaluating the submissions for the whole period of MBT workshops. We also thank the ETAPS organizersfor their assistance in preparing the workshops and the editors of EPTCS for help in publishing theseworkshop proceedings.Alexander K. Petrenko,Holger Schlingloff,Nikolay PakulinMarch 2015References[1] Andreas Blass, Yuri Gurevich, Lev Nachmanson & Margus Veanes (2005): Play to test. Technical ReportMSR-TR-2005-04, Microsoft Research. Available at http://research.microsoft.com/apps/pubs/

A.K. Petrenko, B.-H. Schlingloff & N. Pakulin5default.aspx?id 70129. A short version appears in: FATES 2005, LNCS vol. 3997, pp. 32-46.[2] Igor B. Bourdonov, Alexander Kossatchev, Victor V. Kuliamin & Alexander K. Petrenko (2002): UniTesKTest Suite Architecture. In: FME 2002: Formal Methods - Getting IT Right, International Symposium ofFormal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings, pp. 77–88, doi:10.1007/3540-45614-7 5.[3] Igor B. Burdonov, Alexander Kossatchev, Alexandre K. Petrenko & Dmitri Galter (1999): KVEST: AutomatedGeneration of Test Suites from Formal Specifications. In: FM’99 - Formal Methods, World Congress on FormalMethods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999, Proceedings,Volume I, pp. 608–621, doi:10.1007/3-540-48119-2 34.[4] Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte & Margus Veanes (2001): Conformance Testing withAbstract State Machines. In R. Moreno-Diaz & A. Quesada-Arencibia, editors: Formal Methods and Tools forComputer Science; Proceedings of Eurocast 2001. Available at px?id 77832.[5] Wolfgang Grieskamp, Xiao Qu, Xiangjun Wei, Nicolas Kicillof & Myra B. Cohen (2009): Interaction Coverage Meets Path Coverage by SMT Constraint Solving. In: Testing of Software and Communication Systems,21st IFIP WG 6.1 International Conference, TESTCOM 2009 and 9th International Workshop, FATES 2009,Eindhoven, The Netherlands, November 2-4, 2009. Proceedings, pp. 97–112, doi:10.1007/978-3-642-050312 7.[6] Alan Hartman (2006): Ten Years of Model Based Testing – A sober evaluation. Available at delBasedTestingSoberEvaluation.PDF. Invited talk atthe Second Workshop on Model Based Testing March 25-26, 2006 Vienna , Austria.[7] Thomas J. Ostrand & Marc J. Balcer (1988): The Category-Partition Method for Specifying and GeneratingFunctional Tests. Commun. ACM 31(6), pp. 676–686, doi:10.1145/62959.62964.[8] Alexander K. Petrenko (1993): Test Specfication Based on Trace Description. Programming and ComputerSoftware 19(1).

6PrefaceProgram committee Bernhard Aichernig (Graz University of Technology, Austria) Jonathan Bowen (Birmingham City University, Worshipful Company of Information Technologists, UK) Mirko Conrad (samoconsult GmbH, TU Mnchen, Humboldt University of Berlin, Germany) John Derrick (University of Sheffield, UK) Bernd Finkbeiner (Universitat des Saarlandes, Germany) Lars Frantzen (Radboud University Nijmegen , Netherlands) Ziyad Hanna (Jasper Design Automation, USA) Philipp Helle (EADS, Germany) Mika Katara (Tampere University of Technology, Finland) Alexander S. Kossatchev (ISP RAS, Russia) Victor Kulaimin (ISP RAS, Russia) Bruno Legeard (Smartesting, France) Bruno Marre (CEA LIST, France) Laurent Mounier (VERIMAG, France) Nikolay Pakulin (ISP RAS, Russia) Jan Peleska (University of Bremen, Germany) Alexander K. Petrenko (ISP RAS, Russia) Alexandre Petrenko (Computer Research Institute of Montreal, Canada) Fabien Peureux (University of Franche-Comte, France) Holger Schlingloff (Fraungofer FIRST, Germany) Julien Schmaltz (Open University of The Netherlands, Netherlands) Nikolai Tillmann (Microsoft Research, USA) Stephan Weissleder (Fraunhofer FOKUS, Germany ) Nina Yevtushenko (Tomsk State University, Russia)

Using Model Checking to Generate Test Cases for AndroidApplicationsAna Rosario EspadaMarı́a del Mar GallardoAlberto SalmerónPedro MerinoDept. Lenguajes y Ciencias de la ComputaciónE.T.S.I. Informática University of Málaga [anarosario,gallardo,salmeron,pedro]@lcc.uma.esThe behavior of mobile devices is highly non deterministic and barely predictable due to the interaction of the user with its applications. In consequence, analyzing the correctness of applicationsrunning on a smartphone involves dealing with the complexity of its environment. In this paper,we propose the use of model-based testing to describe the potential behaviors of users interactingwith mobile applications. These behaviors are modeled by composing specially-designed state machines. These composed state machines can be exhaustively explored using a model checking toolto automatically generate all possible user interactions. Each generated trace model checker can beinterpreted as a test case to drive a runtime analysis of actual applications. We have implemented atool that follows the proposed methodology to analyze ANDROID devices using the model checkerSPIN as the exhaustive generator of test cases.1IntroductionAt present, smartphone technology is ubiquitous and changes constantly. Users use their mobiles not onlyas phones, but as compact computers, able to concurrently provide services which are rapidly created,updated, renewed and distributed. In this scenario of continuous evolution, different operating systemshave been developed such as SYMBIAM , IOS , WINDOWS PHONE and ANDROID, which allow phones tosupport more and more complex applications. These platforms define new models of execution, quitedifferent from those used by non-mobile devices. For instance, one of the most defining characteristicsof these systems is their open and event-driven nature. Mobile devices execute a continuous cycle thatconsists of first, waiting for the user input and second, producing a response according to that input. Inaddition, the internal structure of mobile systems is constructed from a complex combination of applications, which enable users to easily navigate through them. Thus, although, at a lower level, the executionof applications on a mobile device involves the concurrent execution of several processes (for instance,in ANDROID, applications are JAVA processes executing on the underlying LINUX operating system), theway these applications interact with each other and with the environment does not correspond with thestandard interleaving based concurrency model.It is clear that the execution of applications on these new operating systems, such as ANDROID [1],may lead to the appearance of undesirable bugs which may cause the phone to malfunction. For example,mobile devices may display the typical errors of concurrent systems such as violations of safety andliveness properties. However, there are other bugs inherent to the particular concurrency model supportedby the new platforms which are not directly analyzable using current verification technologies. For Workpartially supported by grants P11-TIC-07659 (Regional Government of Andalusia), TIN2012-35669 (Spanish Ministry of Economy and Competitiveness), UMA-Agilent Technologies 808/47.3868- 4Green and the AUIP as sponsor of theScholarship Program Academic Mobility.A.K. Petrenko, B.-H. Schlingloff, N. Pakulin (Eds.):Tenth Workshop on Model-Based Testing (MBT 2015)EPTCS 180, 2015, pp. 7–21, doi:10.4204/EPTCS.180.1c Espada, Gallardo, Salmerón & Merino

8Using Model Checking to Generate Test Cases for Android Applicationsexample, applications could incorrectly implement the life cycles of their activities or services (in the caseof ANDROID), or may misbehave upon the arrival of unexpected external events. In addition, conversionerrors, unhandled exceptions, errors of incompatibility API and I / O interaction errors as described in [16]may also appear.Different techniques for analyzing the execution of mobile platforms have been proposed. Verification approaches such as model checking [9] can be applied to the software for mobile devices[22, 21, 19]. Model checking is based on a exhaustive generation of all the inter leavings for the threads/processes. A major problem to apply this technique to the real code, like mobile applications, it theneed to construct a model of the underlaying operating system or libraries [10, 7, 11]. The open nature ofthese platforms, which are continuously interacting with an unspecified environment, makes other analysis techniques such as testing, monitoring, and runtime verification more suitable to check bugs withouttoo much extra effort to model the operating system or the libraries. There have been several recentproposals [12, 24, 18] for testing in this framework with commercial tools [4, 2]. In these approaches,test cases are randomly generated with tools such as M ONKEY and M ONKEY RUNNER [1].Testing and runtime verification maybe also combined, as described in [6], to construct verificationtools for mobile applications [20, 26]. On the one hand, the careful selection of test cases guides the execution of the device, while, on the other, the runtime verification module implements observers devotedto analyzing the traces produced by the device. The runtime verification module was already addressedby some authors of this paper in [14]. Here we focus on describing how the generation of test cases maybe carried out following the model-based testing approach [25] supported by model checking tools.Our proposal is based on the idea that although the interaction between the user and the mobiledevice is completely undetermined, each application is associated with a set of intended user behaviorswhich define the common ways of using the application. For each application, or more precisely, for eachapplication view, we use state machines to construct a non deterministic model representing the expecteduse of the view/application. This state machine is built semiautomatically, with information provided bythe expert (the app designer or tester) and by ANDROID supporting tools like UI AUTOMATORV IEWER.Then, all these view models may be conveniently composed to construct a non deterministic model ofthe user interaction with a subset of mobile applications of interest. Due to the way of building the statemachines, each execution trace of the composed state machine corresponds to a possible realistic use ofthe mobile. Thus, the generation of test cases is reduced to the generation of all possible behaviors ofthe composed machine, which may be carried out by a model checking tool. Although the methodologyproposed does not depend on the underlying mobile operating system, the tool has been built on theassumption that the operating system is ANDROID.The paper provides two main contributions. The first one is the formal definition of a special typeof state machine that models the expected user interaction with the mobile application. The approachto modeling is completely modular in the sense that adding (or removing) new view state machines toincorporate (eliminate) user behaviors does not affect the rest of state machines that have already beendefined. The second one is a method to employ the explicit model checker SPIN [15] that takes thecomposed state machine as input and and produces a significant set of test cases that generate traces forruntime verification tools. We have constructed a tool chain which implements both modeling and testgeneration phases to shows the feasibility of the approach in practice.The rest of the paper is organized as follows. Section 2 describes our approach to using modelchecking for test case generation. Section 3 introduces the testing platform that we are developing.Section 4 provides a formal description of the behaviour of composed state machines. Section 5 useswell known ANDROID applications to describe how our approach for test case generation is implemented.Section 6 gives a comparison with related work. Last section summarizes conclusions and future work.

Espada, Gallardo, Salmerón & Merino12345678910111213141516171819202122239mtype { state init , state 1 , state 2 };typedef Device { byte transitions [ MAX TR ]; short index ; bool finish ; }Device devices [ DEVICES ];mtype state [ DEVICES ];active proctype traceCloser () provided ( devices [ DEVA ]. finish && devices [ DEVB ]. finish ) {end tc : o ut p u t T r a n s i t i o n s ()}active proctype device A () {state [ DEVA ] state init ;do:: state [ DEVA ] state init - transition ( DEVA , BUTTON 1 ) ; state [ DEVA ] state 1:: state [ DEVA ] state 1 - transition ( DEVA , SWIPE ) ; state [ DEVA ] state 1:: state [ DEVA ] state 1 - transition ( DEVA , BUTTON 2 ) ; state [ DEVA ] state 2:: state [ DEVA ] state 2 - transition ( DEVA , MESSAGE ) ; break:: state [ DEVA ] state 2 - transition ( DEVA , BACK ) ; breakod ;devices [ DEVA ]. finish true ;}active proctype device B () {state [ DEVB ] state init ;.devices [ DEVB ]. finish true ;}Listing 1: Sample PROMELA specification for test generation2Model checking for test case generationSPIN [15] is a model checker that can be used to verify the correctness of concurrent software systemsmodeled using the specification language PROMELA. The focus of the tool is on the design and validationof computer protocols, although it has been applied to other areas. SPIN can check the occurrence ofa property over all possible executions of a system specification, and provide counterexamples whenviolations are found.We use the SPIN model checker in our approach for automatically generating test cases from application models in the following way. First, each device will be represented by a single PROMELA process,which contains a state machine that models the applications contained on that device. The state machinesthemselves are written as loops, where each branch corresponds to a transition triggered by an event. Thecurrent state of each state machine (stored as a global PROMELA variable) determines which branchesare active and may be taken. The right hand side of each branch records the transition and updates thecurrent state. This PROMELA specification is explored exhaustively by SPIN in order to generate all possible test cases described by the application model, taking all possible alternatives when there is morethan one active branch at the same time.Listing 1 shows an example of a PROMELA specification that follows the approach outlined above.This example contains two devices and with their corresponding state machine (device A() in line 8and device B() in line 19), with two states plus the initial state. The transition function is used torecord the user or system transition associated with each branch. In order to complete a test case, alldevices must have finished their respective state machines (lines 17 and 22), usually when the do loop isexited (lines 14 and 15). This enables the traceCloser process to be executed due to its schedulabilityrestrictions (line 5), which prints the transitions of the generated test case.In addition to the current state (line 4), this PROMELA specification also keeps a list of the transitionstaken on the test currently being generated (line 2). The purpose of this data structure is twofold. On theone hand, outputTransitions will print the trace stored here. On the other hand, the history of the

10Using Model Checking to Generate Test Cases for Android ApplicationsFigure 1: Architecturecurrent trace is kept inside the SPIN’s global state, which is taken into consideration when deciding if astate has already been visited. Thus, the same transition may be taken more than once if possible (e.g.line 12), since the history of the states will be different. However, this requires the maximum depth ofexploration to be bounded by the MAX TR constant (line 2).3Architecture of

EPTCS 180 Proceedings of the Tenth Workshop on Model Based Testing London, UK, 18th April 2015