The Controlled Calculator: An example of combining models while showing other features of Spec Explorer

The Calculator

The core calculator model is a simple four function calculator. But infix calculators aren't entirely simple, because calculators demonstrate rich variations in outputs depending upon the exact order of input sequences of numbers, operations, and pressing the Equals keys. This implementation (and model) emulates the Windows Calculator. It is similar to but is slightly different from most store-bought calculators, especially in how the Equals key first repeats upon multiple key pushes and how an operation is done when only one operand has been provided. The model and implementation provided, however, should match up with the Windows calculator found under Accessories in the Windows Start menu. The Visual Studio 2010 solution for this example can be found here.

The Scenario

For the purposes of this sample, first the calculator functionality was created as a standalone product. This was then integrated with connection access that allowed the calculator to be used as a service. These were then modeled together as single integrated service. The calculator service model can be explored by itself and its implementation can optionally be tested standalone. The security authorization model controls access to the calculator via a simple minded Access Control List (ACL) consisting of a list of authorized users.  (Note that the full ACL target resources and operations were not of interest for testing purposes so were not modeled). This simplified ACL was modeled on its own and can be explored on its own. Testing the ACL implementation requires the calculator service only for its connection capabilities.

How the Two Model Program Rule Sets Work Together

The ACL (authorization) model and the calculator service model actually synchronize on only a few actions, specifically connection and disconnection. They interleave the rest. The two model programs use the |?| operator to achieve this.  Thus the authorization model can manage its ACL,  allow and release user authorization on its own, as shown by exploring machine AuthorizationSlice, while the calculator model independently can do all of its calculator functionality (actions and events) .  The vast majority of the all-important security related sequencing is done by transition modes in the authorization model. By carefully controlling when the synchronized actions (connect and disconnect) can occur the authorization model imposes the majority of inter-model sequencing constraints expressed by the joint model.  Internally within the calculator service, however, the rules are generally aware that they must be connected to be enabled but have no knowledge at all of the authorization rules.

The end-to end-control is shown, not surprisingly, by machine EndToEndControl (Slice and Test) in the Cord file. It specifies that between ACL creations and disposals, users can be authorized multiple times, and between multiple authorizations the current user can connect multiple times, and within a connection multiple operations can be performed.  This models the functionality of the core authorization sequences. Multiple simultaneous users and connections were not modeled. Had this been a test objective, likely instance based modeling would have been used and the implementation would be have been multithreaded. The current model (and the current implementation) adequately tests basic end-to-end functionality.

How the Implementation Does This

The implementation is written as four layers. The top level static class acts as the interface that implements the controllable and event actions declared in Cord. Thus it can be considered to be an adapter layer. The rest of the implementation is written as three layers, each of which is represented by a single object. There is an object that implements all of the calculator functionality, one that manages the connection to the calculator object, and finally one that represents the ACL control logic. In principle, the calculator object could be replaced by the real Windows calculator, but that has not been attempted.

Things to look for

In addition to modeling the active (behavioral) joining of two rule sets, this sample illustrates several important features of using Spec Explorer.

Cord

The Cord file is structured around logical groups of configurations, which of course is what configs are supposed to do for a living. The use of parameters in machines is shown by the DoubleOperand machine. The machines related to test purposes are built up from scenarios to model slices to test cases. For example,  BigLongScenario to BigLongSlice to BigLongTest. There are a number of helper machines such as FullStart, CloseDown, SingleOperation. Fairly rigorous testing of calculator key sequences is shown by all the scenarios that  are included in AllOperationsTogetherSlice (and Test).

But in many ways the most interesting machines deal with constructing and joining the two rule sets. The machine called AuthorizationSlice builds the (sliced) ACL model program and CalculatorService constructs the model program of the calculator service. These two model programs are actually independent of each other and use their own rule sets kept for convenience in separate name spaces and files. They make no assumptions about each other.

Machine JointModel is the one that joins the two by means of the partially synchronizing |?| operator, aka the “synchronized-interleaved parallel composition operator”.   This synchronizes when both machines try to produce the same action just like the parallel synchronization operator ||-- in this case the connection and disconnection related actions--but interleaves otherwise when either machine produces an action unique to itself, just like the ||| operator. It may be that |?| is one of the more underappreciated operators in Cord.  There are subtleties in its definition, but it is behaviorally powerful as shown.

Machine SimpleDirectSlice (and Test) deserves quick mention. If uncommented in CalculatorService.Connect (file Calculator.cs), the implementation will allow the calculator service to be tested on its own by automatically creating an ACL and authorizing a fictitious user. (The users defined for model slicing in configuration Authorize are neither fictitious nor necessarily innocent but that's another story.) This implementation short circuit would ordinarily be a security hole, since the ACL logic is being neutered, but is useful for testing and illustrates one way to get around the layering of the implementation code. Note that no changes were necessary in the CalculatorServiceModel rules to make this test generation work correctly because those rules by themselves do not depend on the ACL logic to which they are later composed only by the |?| operator

Model and Implementation Code

The model and implementation code is heavily commented and largely self-explanatory.  The model code uses helper functions extensively. In both the model code and the implementation, state data is initialized actively in a constructor or other method. This promotes consistency and successful re-running of the same code in a test sequence or between test case executions.

Note that a rule may be blocked from producing a step in a helper function such as in CalculatorServiceModel.RequiresConnected (in file ArithmeticRules.cs).  A rule method must reach all the way to an exit point without violating any Condition class constraints in order for any step(s) to be produced. Otherwise that rule execution is completely discarded during exploration and no step is produced outgoing from the current state by that rule.

In the same model rule set, the rule for the Divide action shows how a special condition, often an exception, can be converted into the expectation of a following event. Spec Explorer actions are indivisible which means they cannot suddenly be stopped and switched to another one. But at model evaluation time, the new state can reflect that a condition has occurred in the prior step (from a prior rule firing). In this case, the rule for OperationError will pick up on that fact that previously Divide had found and marked that the denominator was zero. A quick look at the configuration called Operation in Cord shows that the OperationError action is to be treated as an event. This is the only place to find out that the OperationError rule described an event, as it does not matter to the rule itself whether it is an input or output action to the SUT. Rather, the rule just knows under what conditions that the step can be seen externally to the SUT.  It does matter, of course, to exploration and test code generation both of which will treat the event appropriately (which is why the Cord code tells them).

The actual implementation of the OperationError event can be found in CalculatorService (in file Calculator.cs). Notice it requires an instance of the correct name (OperationError) of a correct kind of delegate type. In this case it happens to be called OperationErrorHandler, but the type name may be chosen at will. The event is actually raised in this sample by helper method CalculatorService.RaiseError which is a callback used by the calculator object if it encounters a problem with divide by zero. The event will be placed on Spec Explorer's run time event queue for future consideration and the Divide action will run to completion, returning a zero value if a problem occurred as tested by scenario DividebyZero in Cord. When the model indicated the event would be eligible for consideration the queue will be examined and in the two cases of the ZeroDivide scenario it will be found. The third case does not look for the event and shows that a test may conclude successfully in an accepting state even if there are events left on the event queue.

Part of the moral of this story is that controllable actions (that is, inputs to the SUT) in the implementation are simple methods, but observable actions  (that is, events) are implemented quite differently (as described above).  Whereas in the rules, such actions are indistinguishable.  And only in Cord, as the bridge in between, does Spec Explorer learn which is supposed to be which.

Comments

• Anonymous
  March 30, 2011
  maybe not...for some reason errroreedd on first try

• Anonymous
  November 18, 2012
  Hi The link to the solution file is broken. Please update.