The successful application of model-based testing (MBT) heavily relies on constructing a complete and coherent model of a system. This implies that inconsistency, incompleteness, or inaccuracy due to human error bear signi cant consequences. We propose a formal framework for MBT which we call AHR: agile, human-centred and re nementoriented. AHR captures an iterative construction of models and test plans, as well as supports re nements at di erent levels of abstraction.
Model-based testing (MBT) is a technique for generating test cases from system
model. Testers using this approach concentrate on a data model and generation
infrastructure instead of hand-crafting individual tests, cf. [
Construction of complex models heavily relies on tacit human knowledge and
therefore will always remain the task of a human tester, escaping full
automatisation. The complexity and error-prone nature of this task, however, calls for
Copyright ' by the paper's authors. Copying permitted only for private and academic
purposes.
more emphasis on human-centred approaches in automatic support of
modelbased testing. There are numerous works on human error in software
development [
In this paper we introduce AHR (agile, human-oriented, re nement-oriented),
a formal framework for integrating human-centred considerations into MBT with
multiple levels of abstraction. This framework extends the ideas of
HumanCentred Agile Test Design (HCATD), cf. [
The proposed AHR framework has three core features: A Agile: Both the test plan and system model at each abstraction level of modelling/implementation are agile in the sense that they are (only) su ciently complete, accurate and consistent (with coverage requirements); error correction and speci cation extension are iteratively performed.
H Human-centred: Error correction and speci cation extension/completion can be supported by posing series of queries or issuing alerts to the tester. R Re nement-oriented: Re nement is performed in the framework in several ways: (i) the usual static re nement of system properties when moving between abstraction levels, (ii) dynamic re nement of system properties and test plans as a result of information completion or error correction. Let S be the system under test. Assume that we construct a model with m levels of abstraction. We say that S can be completely described at each level l by the set PROPl(S) of its properties. The main two tasks of the human tester in the process of MBT are (1) to construct an appropriate abstraction M of S, and (2) to propose a test suite that validates S against M according to some chosen coverage requirements. For performing the task (1), we have to decide which properties of the system are important to model/implement (and, respectively, to test) and which need to be abstracted away. Thus, we have to partition the set PROPl(S) into two disjoint subsets: LPROPl(S) { the properties to be modelled/implemented and tested, and ABSTRl(S) { the properties to be abstracted away, knowingly or unknowingly.
LPROPl(S) [ ABSTRl(S) = PROP(S)
LPROPl(S) \ ABSTRl(S) = ; The properties LPROPl(S) might include the pre- and post-conditions of actions. We denote the pre- and post-conditions of an action Act on the level l by P rel(Act) and P ostl(Act) respectively.
On each abstraction level the traceability between the system properties and the corresponding tests is crucial for our approach (cf. also Figure 1). If the information is not important on the current level, it could in uence on the overall modelling result after some re nement steps, i.e., at more concrete levels that are closer to the real system in the physical world. Therefore, while specifying system we should make all the decisions on abstraction in the model transparent and track them explicitly. In the case of contradiction between the model and the real system this would allow us to nd the problem easier and faster.
VALIDATED1
REJECTED1 UNCERTAIN1 TESTS1 TESTS2 TESTSm-‐1 TESTSm VALIDATED2
REJECTED2 UNCERTAIN2
… VALIDATEDm-‐1 REJECTEDm-‐1 UNCERTAINm-‐1 VALIDATEDm REJECTEDm UNCERTAINm
HCATD correct HCATD correct HCATD correct HCATD correct
LPROP
V1 LPROP
V2 …
Level 1 ABSTRKNOWN ABSTRUNKNOWN Level 2 ABSTRKNOWN
ABSTRUNKNOW N Level m-‐1 ABST RKNOWN ABSTR UNKNOWN Level m ABSTRKNOWN
ABSTRUNKNOWN LPROP Vm-‐1 LPROP
Vm To introduce an explicit representation of incompleteness, which is manageable and traceable at di erent levels of abstraction, we suggest to divide the set ABSTRl(S) into two disjoint subsets, ABSTRKNOWl(S) and ABSTRUNKNOWl(S): ABSTRKNOWl(S) [ ABSTRUNKNOWl(S) = ABSTRl(S)
ABSTRKNOWl(S) \ ABSTRUNKNOWl(S) = ; This allows us to separate the properties of the system from which we abstract intentionally from those, from which we abstract a unknowingly. The ABSTRUNKNOWl(S) properties are not identi ed/classi ed at level l due to lack of information (which may be due to error/omission). Thus, on each level l we generally operate with three sets of properties: { LPROPl(S) { properties the tester decided to include at this level, { ABSTRKNOWl(S) { properties from which he knowingly abstracts at l; { ABSTRUNKNOWl(S) { properties which he unknowingly abstracts at l. With each re nement step the tester moves some part of system's properties from the set ABSTR to the set LPROP. We can say that in some sense the set ABSTR represent the termination function for the modelling process.
In a similar manner, the set of all tests is divided into three mutually disjoint subsets on each level l: { validatedl: the tester con rmed these tests as executable on this abstraction level according to some chosen con rmation strategy; { rejectedl: the tester rejected these tests as impossible or irrelevant on this abstraction level; { uncertainl: the tester has not classi ed these tests to be validated/rejected, as not enough information has been provided for the classi cation. 3
A type of MBT which uses particularly simple models is combinatorial test
design (CTD), cf. [
One of the most standard coverage requirements is pairwise testing [
Typically, the CTD methodology is applied in the following stages. First the tester constructs a combinatorial model of the system by providing a set scenarios which are executable in the system. After choosing the coverage requirements, the second stage is constructing a test plan, i.e., proposing a set of tests over the model, so that full coverage with respect to a chosen coverage strategy is achieved. The set of parameters A as well as the sets of corresponding values V will be re ned and extended along with the re nement and extension of the sets of properties. Respectively, the sets of tests have to be also re ned. When a new level l + 1 is created by specifying LPROPl+1 and Vl+1, and some parameters and their values are unchanged while re ning the system from level l to level l + 1, then a number of corresponding tests are still unchanged too, which means that we can also reuse their marking as validated/rejected/uncertain. If we trace the re nement relations not only between the properties but also between test plans, this might help to correct possible mistakes more e ciently, as well as provide additional support if the system model is modi ed. In AHR, we use upper indices on the test names to denote that the test belongs to a particular abstraction level, e.g., test35 would denote that the test5 de ned on the Level 3. 4
An important domain in which modelling with di erent levels of abstraction
is particularly bene ciary is cyber-physical systems (CPS). Our early work on
speci cation of CPS on abstract level was presented in [
Let us consider a cyber-physical system system with two robots R1 and R2 interacting with each other. Using the AHR framework, we model each robot on Level 1 by two parameters, GM and P : { GM represents the mode of the robot's grippers, which can be either either closed (to hold an object) or open. We specify two system parameters of this type on Level 1, GM1 and GM2 specifying the gripper modes of R1 and R2 respectively, where V(GM1) = V(GM2) = fopen; closedg. { P represents the robot's position. On Level 1, we assume to have only three possible positions for each robot. In the system model on Level 1, we have two system parameters of this type, P1 and P2 specifying the positions of R1 and R2 respectively, where V(P1) = V(P2) = fpos1; pos2; pos3g. In what follows let us assume pairwise coverage requirements. We specify two meta-operations Give and T ake to model the scenario when one robot hands an object to another robot. A meta-operation Give in which R1 gives an object to R2 can only be performed when the gripper of R1 is closed, the gripper of R2 is open, and the grippers of both robots are in the same position. This means that not all test cases are executable and further restrictions should be imposed. Suppose, however, that the information on the position is erroneously omitted, because of a human error on speci cation level while de ning the set of LPROP1. Thus, LPROP1 = fP re1(Give)g, where P re1(Give) = fGM1 = closed; GM2 = openg. This induces a system model with the corresponding tests (cf. Table 1). Initially, all tests are be marked as uncertain. The tester then goes on to construct a test plan by selecting two tests from the table, for example, test1 and test5. In this test plan, the tester erroneously omitted a test case including pos3. Once the tester submits the test plan, test1 and test5 are marked as validated. At this point the tester's mistake may be discovered, as pairwise coverage is not achieved: e.g., the interactions fP1 : pos1; P2 : pos2g and fP1 : pos3; P2 : pos3g remain uncovered. This can be either due to the fact that the tester considered non-executable tests as possible or forgot to add some tests.
A human-oriented solution to this kind of problems would be issuing a query to prompt the tester to either extend the logical condition with P1 = P2 (thus removing the interaction fP1 : pos1; P2 : pos2g from coverage requirements) or extend the test plan with test9. To provide a better overview of the plan conditions while analysing whether a new conditions and/or tests should be added, we also suggest to provide an option show the current conditions. When the tester decides to mark test9 as validated and to add the logical condition P1 = P2 to the set LPROP1, the framework will update the set LPROP1 and notify the tester that the pairwise coverage is achieved under the current selected conditions. After the corresponding corrections, LPROP1 = fP re1(Give)g, where
P re1(Give) = fGM1 = closed; GM2 = open; P1 = P2g
As the next step, the framework reminds the tester that a number of tests are
still marked as uncertain (cf. Figure 3). The tester might either accept with the
current marking or mark all the uncertainties as rejected to switch to an
optimised view, where only validated tests are presented to increase the readability.
P1
pos1
pos1
pos1
pos2
pos2
pos2
pos3
pos3
pos3
This paper3 introduces the AHR framework for supporting an agile MBT. The
framework explicitly acknowledges that the human tester as well as the system
designer may make mistakes that need to be corrected. Error correction and
speci cation extension/completion is supported by posing series of queries or
issuing alerts to the tester. AHR involves several abstraction levels of modelling
and testing, where models and test planes can be iteratively updated, completed
and improved during the development process. To illustrate the core features of
the framework, we have presented an example scenario from the domain of cyber
physical systems. AHR has the potential to facilitate the adoption of MBT in
industry, increasing the e ciency of the human tester and providing opportunities
for collaborative e orts. To increase the productivity of our approach, we might
embed it into facilities as the Virtual Experiences Laboratory [