Modeling Stochastic Systems in Spec Explorer

One of the more advanced – and powerful – features of Spec Explorer is its ability to handle stochastic SUTs. Stochasticity is common in systems with external dependencies, this could for example be the file system, network interface or external devices. Common for all these dependencies is that they sometimes fail for various reasons. You cannot predict when this will happen, and for the most part in Software testing we strive to avoid these spurious behaviors at all cost.

Another source of stochasticity is the use of random in the SUT (which I will explore a bit more in this post) or stochastic behavior due to race-conditions in multi-threaded applications (which I will investigate further in a later post).

First of all, what does a stochastic model look like? Take a look here:

This picture represents a model of a stochastic accumulator. It shows a slice where the accumulator is increased twice then reset. Each addition is stochastic in that it can add either 1 or 2 to the counter.

When working with stochastic models, in addition to the normal “round” states, Spec Explorer introduces diamond-shaped decision states. Each diamond represents a choice in the model where the SUT can behave in one of many ways. In the case of the stochastic accumulator we can see that the value of the accumulator can go from the initial value of 0 to either 1 or 2 in the first addition step.

Re-Modeling the Traveling Salesman – Part II

Last time we had a look at a very crude model for growing graphs for the Travelling Salesman Problem (TSP). I neglected to actually visualize what the solutions looked like, so here is a rendering of a couple:

Not very complex indeed... So what seems to be the problem here? Well, the model itself is very exhaustive, so it will generate any conceivable graph on the input domain. The single model rule is generic on the full input domain:

config Grid20x20: Main

{

    action abstract static void TravelingSalesman.InsertVertex(int x, int y)

        where x in {0..19}, y in {0..19};

}

This means that for each state Spec Explorer will try X * Y rules, so for larger input domains like 20x20, it takes forever to explore a state fully. What we are interested in with the TSP is not to construct a plethora of simple graphs, but to generate high complexity graphs (because they are much harder to solve). So what we need is a depth-first search (DFS), luckily Spec Explorer allows us to do just that using a config switch:

config Main

{

    ...

    switch DepthFirst = true;

    ...

}

Unfortunately it turns out that the DFS exploration uses an “optimized” version of DFS, causing it to always fully explore each state it visits, instead of immediately exploring from newly discovered states. Not that it’s going to show the extra states that got explored, they are simply hidden away until they get fully explored much later in the process (sorry, guys but that’s just silly). Anyway, that is exactly what we wanted to avoid, because even when using DFS exploration on a 10x10 grid it will take hours to generate graphs with 10 vertices.

Modeling the Traveling Salesman

I’m going to attack a well-known problem from the 1800 century in this post: Traveling Salesman Problem (TSP).

The objective in the traveling salesman problem is to find the shortest path through a network graph visiting every node/vertex exactly once and returning to the origin, such a path is called a tour of the graph (or a Hamiltonian cycle if you are into computer science). The problem is NP-hard to solve, meaning it is likely that no feasible exact solution exists for large graphs. There exist a lot of variant on the traveling salesman problem. I will consider the form of the problem in which the graph lies in a plane, also known as the Euclidian TSP. This puts constraints on the distances between nodes and is a symmetric formulation of the problem. But still, this is an NP-hard problem.

To put things into perspective, the number of distinct Hamiltonian cycles through a graph is:

Enumerating all possibilities becomes infeasible for even small graphs. For n = 21 the number of solutions is 1,216,451,004,088,320,000. For the case of n = 101 the number of solutions is approximately 9e+157 which exceeds the approximated number of atoms in the known universe. Of course, I’m not claiming to solve this problem – actually I’m not trying to solve it at all. Many better people have tried that before me. I’ll however focus on testing a TSP solver. It may be exceptionally difficult to solve the problem, but it is possible to construct graphs for which the solution is known (and non-trivial) without too much effort. A model for that could look like:

I plan on doing a series of posts on this problem. In this first post I will define the problem and the method in which I’m constructing a graph for the TSP. In the following posts I will investigate different models for growing TSP graphs, and look into how they perform.

Model Slicing with Spec Explorer

It’s been some time since I had the chance to blog on MBT. January 2^nd 2012 my second son was born, and I’ve been on three weeks of paternity leave. Since then I’ve been too busy at work to squeeze in time to play with MBT, but now I’ve finally managed.

Today I want to talk about model slicing which is one of the more advanced features of Spec Explorer. Slicing is extremely powerful, because it allows you to build your models very generically, and then create many slices of that model with differing purposes.

I’m going to show some very simple examples on how slicing works, and then I will dig up the Binary Search Tree model to illustrate how this would work in practice.

Slicing

For my example on slicing I’m going to construct a very simple model. The state is one integer variable, and I have two rules defined the following way:

        [Rule(Action = "A()")]

        static void A()

        {

            value *= -1;

        }

        [Rule(Action = "B()")]

        static void B()

        {

            value++;

        }

Rule “A” flips the sign of the value and “B” increases it by one. The state space of this model is infinite. If you explore it you get something like:

Are Test Oracles a mathematical nicety to cover-up problems?

Last week I had an interesting discussion with a colleague that did not agree with my take on Model-Based Testing. He was unwilling to buy my arguments for why Model-Based Testing is a more efficient way of automating test cases compared to traditional scenario automation. He was a firm believer in Model-Based Testing but his experiences told him that modeling was an expensive cost up-front, which could be made up for in maintenance savings, whereas I claimed that modeling was a much cheaper automation approach.

Furthermore, he argued that my model was close to useless, because it did not come with a validation oracle. At a deeper level, the discussion also revealed some interesting discrepancies to me: He believed.

Needless to say, we never reached agreement on the subject – but I realized later on that we were arguing from completely different perspectives.

After the discussion I started thinking: “How can we be of so differing opinions?” After fumbling around with this question in my head over the weekend, I realized that we were using Model-Based Testing for two completely separate purposes.

A notion started to form in my head – it seemed that there were different ‘schools’ (or views) within Model-Based Testing.

·         Theoretical modelers: They want strict rules around their models, and conduct rigorous validation in an effort to validate the conformity of their models. They have a theoretical approach to software testing and like to mathematically prove algorithms and construct test cases that cover just the necessary and sufficient cases.

·         Pragmatic modelers: They are more of the ad-hoc modeling type. They have a pragmatic approach to Model-Based Testing in which a model is valuable on its own. They understand that the model should be validated, but they can live with limited validations. They see value in the model as a means for communication.

Requirements and Model-Based Testing: A rocky road

This post is on something that has been bogging my mind a lot lately, which I haven’t been able to fully express, but I’m hoping getting it published will help me settle my mind.

I had the pleasure of attending the ETSI Model-Based Testing User Conference – and let me start by giving kudos to all the great people in the field attending and giving some sharp presentations!

At the conference I got a look into all the available vendor tools for Model-Based Testing (I won’t list them here; this is not supposed to be an advertisement blog). All of them are pretty powerful tools, and they allow you to build models from a set of requirements that you gather in the beginning. In the model you specify which actions corresponds to a certain requirement – e.g. in finance you may have a requirement that posting a sales order will produce a set of ledger entries so this requirement would be associated with the posting action. Some can even import your requirements from external tools, and keep track of changes to requirements. This is all pretty nice, and one tool showed the ability to visualize the impact of a requirement change directly in the rendered model view – now that is awesome!

A significant number of presenters at the conference were also happy to report that they had discarded existing metrics for quality of their software testing, and replaced it with requirements coverage. Meaning, they now record the number of times requirements are covered in their generated test suite.

But then a thought came to me:

“If I know all my requirements up-front, why would I use Model-Based Testing instead of just writing one or two scenario tests per requirement, which I know covers these requirements well?”

Model-Based Testing of Legacy Code – Part I

It has been a while since I had time to post on this blog. I've been kept busy attending the Model-Based Testing User Conference - it had some really great presentation, that I also want to find some time on reporting on. I have a trip report ready, but I need to boil it down to the relevant stuff before I post it here. Granted, my next post is not going to be on Model-Based Testing, but it will however be the first in a series of posts that - with a bit of luck - will build up to some really interesting Model-Based Testing!

That being said, let's jump into it. Recently I’m being faced with a challenge of taking a large set of legacy code changes and test it in a way that is sensible. I work with a colleague in a two man team on solving this problem.

You can think of the changes as a source control branch. The root branch has good test coverage, but the new branch has no automated test coverage. The changes contains both added functionality to the product, but also smaller tweaks to existing code in the form of changes to existing functionality and regulatory changes.

The objective is of course to apply Model-Based Testing somehow, but the major challenges are:

A)     How do we make sense of this new branch?
B)     How do we approach automation of legacy functionality?
C)     How much can be obtained from modeling?

I will be writing a few blog posts for the coming weeks on the progress we make as we go along, but ultimately I would like to hear from my readers, what ideas they have on how to tackle this problem.

So let’s start with the first challenge...

How do we make sense of this new branch?

We decided to analyze the changes and group them into two sets: Features and integration points. A feature is a coherent set of changes that was developed in the same go, whereas integration points cover the incoherent changes that are either smaller or made over a longer period of time. Later we will see how this categorization affects the automation strategy we would like to apply.

Luckily we have documentation that names these features and link them to source files, so we do not have to make a detailed analysis to uncover what is coherent and what is not. Some documented features are small and can be seen more as integration points.

All integration points can be identified through a simple source code difference analysis. Notice this includes all features as well. It’s an open challenge how to identify overlap...

This was a brief introduction to the upcoming project from my side.

The next step that we are working on is coming up with a structured approach on how to handle legacy code, where we build a risk profile over the changes, more on this next week...

Dealing with floating points in models - Part II

Today I’m going to follow up on Part I, but I’ll give you the implementation details of the classes. I provided you with a generic interface:

IDomainVariableSampler<T>

Now as I pointed out previously, we can choose to implement this interface for any domain type, so let’s try implementing it for a double domain:

    public class DomainDoubleSampler : IDomainVariableSampler<double>

    {

        public double Maximum { get { return 100.0; } }

        public double Minimum { get { return -100.0; } }

        public double BoundaryNegative(double boundary)

        {

            return boundary - double.Epsilon;

        }

        public double BoundaryPositive(double boundary)

        {

            return boundary + double.Epsilon;

        }

        public double Sample(double lowerBound, double upperBound)

        {

            Random rand = new Random(1);

            return lowerBound + rand.NextDouble() * (upperBound - lowerBound);

        }

    }

This implementation defines an input range of [-100.0, 100.0] and is sampling at random inside partitions of this interval.

James D. McCaffrey implements Recursive Binary Search Tree

Today I came across this blog article by James D. McCaffrey, where he actually implements a recursive binary search tree, and I couldn’t resist the urge to apply my own Model-Based Testing solution [1,2] to his implementation!

I had to extend his solution a bit to allow for an internal validation function of any constructed tree, but besides from that my only comment to his solution is that he treats error conditions by silently ignore them – that is the following actions generate no errors/exceptions:

A)     Deleting an element that does not exist in the tree.
B)     Inserting an element twice into the tree.

Patching these up in his code, my model generated test cases all passed, so his implementation is rock-solid! Kudos for that!

References:

[1] Application of Model Based Testing to a Binary Search Tree - Part I
[2] Application of Model Based Testing to a Binary Search Tree - Part II

Domain input partitioning / dealing with floating points in models – Part I

Originally I wanted to post everything in one article, but it got too long, so I decided to split it and save the hardcore details for the next post.

I find that dealing with models involving floating point input can be a tad tricky, so why not post on this topic? The problem here is infinity. It stems from the fact that any given slice of a floating point argument is of infinite size (or at least close to). Often when working with integer models we limit the input variables to a specified range like: where x in {0..2}. However, this does of course not work if x is a floating point input.

So how do we deal with infinity? First of all we need to clarify what it is we want. Clearly we do not want to test every possible floating point values between 0 and 2. Also, what we want is determined by what we are testing. So let’s make up an example. Assume we are to test the square root function (of real values to keep it simple), what kind of inputs would we give it? If you are a software tester your testing aptitude should kick-in right about now. We want to try a sunshine scenario with a positive value. We also want to make sure any negative input gives an error and also the boundary case 0 gives an error. Then we also have some extreme ranges like a very large positive number, a large negative number and the maximum and minimum values of the input type.

If we analyze our pattern here, all we are doing is partitioning the input domain. If you have been following this blog for a while you may recall I referenced equivalence class partitioning before – this is the same stuff. Simplifying a bit we end up with an input domain like:

The important part here is that we have fixed points of interest (the boundaries) and between we have ranges. For the boundary cases, besides the actual boundary value of interest is the near neighbors ±e, where e is a very small number. For the ranges we do not really care what the exact number is, for want of better we draw a random sample from the region.

Note on Spec Explorer and small floating point values:

Unfortunately I found a bug in Spec Explorer, that it crashes when working with small values in floating point. This limits me from trying out combinations where the parameter is e. The implementation of the automatic domain partitioning will thus also be limited to testing only at boundary cases and not their near neighbors as well.

Multi-Threaded Modeling – Barrier Synchronization

Okay, all my previous posts have been based on static system models, where rules and actions are static functions in classes. A lot can be accomplished with this, and it is also possible to wrap instance based applications inside static functions. However, Spec Explorer allows us to work with actual instance based models.

So what does this mean for us? Well, it means we are allowed to instantiate any number of objects of some type and Spec Explorer can reference each of these objects individually. For example, you could write a class that represents a complex number, and have Spec Explorer create two instances of this object and then add them together. This would be a basic example, but instead let’s jump to something more tricky – multi-threading!

You can imagine that instance based modeling and multi-threading are closely related. But there are some key issues one must understand first. Instance based modeling is not multi-threaded, it is exactly as sequential as any static model. Spec Explorer will not create a new thread for you when you instantiate an object. Any interaction by Spec Explorer will be from the “main”-thread, you have to handle communication with your threads.

Barrier synchronization

The example I have picked for this post is a barrier synchronization implementation. Barrier synchronization is a pattern for worker threads in multi-threaded application. With barrier synchronization each thread must wait for its co-workers to complete their cycle of work before the next cycle starts. Denoting the number of cycles completed by thread i as c_i, this can be stated by the following invariant:

          

Essentially each thread reaches a “barrier” upon completion of its work. This “barrier” is only lowered once all threads have reached it. Upon release of the “barrier” the worker threads continues their work.

Model-Based Testing in Agile Development Cycles – Part II

Last post I left you hanging after a model had emerged from our initial acceptance requirements. The model we generated looked like:

Today’s post is about what you can use this model for in agile development, and what kind of test cases it produces.

Design discussions

As I already pointed out in the previous post, models are great in discussions. Often when you explain the model to the product owner he/she will start noticing quirks. For the example model we developed, one such quirk is that the system is not allowed to reverse a payment if said payment has been involved in a financial application. Although it is a requirement in the system, it was not mentioned in the acceptance criteria because it is not a sun-shine scenario. Design discussions based on models will help you uncover these implicit requirements.

Model-Based Testing in Agile Development Cycles – Part I

Today I’m strafing away from Model-Based Integration testing as I’d like to ramble a bit about using Model-Based Testing in an Agile development cycle. For those few of you who haven’t heard about Agile, here’s my crude and narrow look at it.

Agile development

Agile development is often referred to as Scrum, however Scrum is just one Agile methodology, many more exists. In Agile development work is broken up into short sprints of roughly two weeks duration. At the beginning of a sprint you sit down with your team (size 4-7 roughly) and plan what you believe you can achieve during the next two weeks. The main idea is that when you complete a sprint you are done. In contrast, way too often in waterfall you hear the developer/tester saying I’m done (or “almost done”) and what they mean is that the code is done, but they need to run tests, validate performance, security, stress, etc. That does not fly in Agile, done means done, your code is ready for production. The idea of course, is that you do not have to go back and revisit your work at a later point in time – it is Agile because you do not drag a huge backlog of items you need to do when you enter the next sprint.

Okay, enough about Agile – there are lots of other (and better) sources out there online [1] and in books [2].

Model-Based Testing and Agile

Recently I’ve gained some experience applying Model-Based Testing in an Agile development cycle. It’s tricky business and you have to balance your time carefully. There are definitely some pros of applying Model-Based Testing in Agile, but one has to be very careful not to focus too much on modeling through the sprint - instead I suggest taking the time early on in the sprint to formalize a model, which servers as a good aid in discussions as well as a great reference tool later on.

Model-Based Integration Testing – Part II (State encapsulation)

Last time we saw how we could perform Model-Based Integration Testing of a FileSystem model and a Network model using extension models. One problem with this approach was that the first model had to expose its internal state to the other model. In this post I’m going to talk about model state space encapsulation.

A step in the right direction is to do model encapsulation. Let’s start out by obtaining the same model results but having the FileSystem model encapsulating its state. Simply change accessibility of all internal state variables to private:

        private static int drives, currentDirectory;

        private static SequenceContainer<int> directories = new SequenceContainer<int>();

Now of course our Network model won’t compile, as it was referencing the FileSystem state variables directly. We have to realize what the common concept is here – the Network layer is supposed to mimic a directory structure and to do this it must have an interface to create a drive in the FileSystem models state space. One easy way to obtain this is to increase the accessibility of the CreateDrive rule to public, so the Network model can directly call a rule in the FileSystem model:

        [Rule(Action = "MapNetworkDrive()")]

        static void MapNetworkDrive()

        {

            FileSystem.CreateDrive();

        }

Model-Based Integration Testing – Part I

First let me introduce the concept of integration testing. Integration testing opposed to unit testing is all about the big picture, and is designed to verify that components of an application are working together correctly. Take Windows as an example. The operating system has literally tons of components, and many of these interconnect.

One such example could be when you map a network drive on your computer. The network layer integrates into the file system by creating a virtual drive, while the file system integrates into the network layer by reading network paths. The actual network location is integrated into your file system and displayed as a drive icon under My Computer. Even though the networking layer and file system layer are both tested in isolation, there is no guarantee that the two components will work together once they are connected to each other. A ton of problems could occur in this integration! Integration testing is all about finding such issues.

Model

Let’s start by modeling a file system. We model the following:

    static class FileSystem

    {

        ...

        [Rule(Action = "CreateDirectory()")]

        static void CreateDirectory()

        {

            ...

        }

        [Rule(Action = "ChangeDirectory(directory)")]

        static void ChangeDirectory(int directory)

        {

            ...

        }

       

        [Rule(Action = "CreateFile()")]

        static void CreateFile()

        {

            ...

        }

        [Rule(Action = "CreateDrive()")]

        static void CreateDrive()

        {

            ...

        }

        [Rule(Action = "FilesOnDrive(drive)/result")]

        static int FilesOnDrive(int drive)

        {

            ...

        }

    }

The idea here is of course that we have a file system, with a default drive (say “C:\”). We can create new directories and in these we can create files, we also have a validation function that counts the number of files on a drive.

T-wise combinatorial Model-Based testing – Part II

In the previous post we saw how Model-Based Testing can be used to generate combinatorial input to the SUT. This is very nice, because we can capture this behavior in a generic way, and easily extend it, and the model will automatically generate the necessary combinations.

One of the oddities we observed, however, was that the model generated equivalent test cases where the parameter order was swapped. For pair-wise testing this is an annoyance because the model generates double the number of necessary tests, but for higher orders of t this leads to big problems as the duplications scale as n x t! (that’s t-factorial!), where n is the number on unique tests and t is the dimensionality of the combinatorial test generation.

T-wise combinatorial Model-Based testing – Part I

One of the strengths of Model-Based Testing is the ability to generate combinatorial inputs from a model. Say for example we are using a black-box testing approach on a scientific implementation of the inverse of a multi-dimensional matrix function:

               

The SUT is designed to compute the inverse of f(x,y,z) for any value of x, y, z. We may state the test invariant that

            

Which states that the matrix product should not differ from the identity matrix by more than some small residual error. The nice thing about matrix inverse is the relative simplicity in verify the correctness of the implementation, because direct matrix multiplication is simple.

The actual setup is somewhat constructed, but it serves as a good example. The point is that we are testing an implementation on a multi-dimensional function (in this case 3-dimensional). Keep in mind that the SUT could be any function that requires more than one input.

We Are Going To Berlin

We got some great news to share! Apparently the ETSI board liked our abstract on Model-Based Integration Testing so much they decided to grant us a 20 minute presentation slot at the 2011 Model-Based Testing User Conference in Berlin on October 18-20^th (which I previously announced on the blog).

Seeing how this idea on Model-Based Integration Testing has been blue-stamped by an authority, I thought it would be a good idea to share some of the details of our framework over a series of upcoming blog posts. The plan is to reveal some more details here that can be presented in 20 minutes. Then I will be able to refer participants to this blog for more details.

The basic idea of the framework is to generate model based tests that span multiple feature boundaries within the SUT. We obtain this behavior using a producer/consumer pattern on “Universally Recognized Artifacts” (URAs) which are cleverly chosen pieces of information inside the SUT that “resides on the boundaries of system features”.

For now, we are very excited about this, and looking forward to a great conference!

Applying Model-Based Testing for Fault-Injection in cloud services – Part III

2-services model

Interestingly enough, when modeling more than one service, the model will also generate tests that verify services continue functioning even when others go down. Essentially what we are checking here is that we don’t have any unnecessary dependencies between the services, and that a service won’t hang because another one is down.

When designing models including more than one service the state-space can rapidly explode. Consider adding just another service: Payment Service into the model which we depend on upon check-out.

We extend our model by adding:

    public class PaymentService : ModelService

    {

        public override string Name { get { return "Payment"; } }

        public void ProcessPayment()

        {

            ConditionRunning();

        }

    }

And changing the model to:

    static class WebshopModelProgram

    {

        static ShoppingCartService cartService = new ShoppingCartService();

        static PaymentService paymentService = new PaymentService();

        [Rule(Action = "AddToCart()")]

        static void AddToCart()

        {

            cartService.AddItem();

        }

        [Rule(Action = "ProceedToCheckOut()/result")]

        static bool ProceedToCheckOut()

        {

            if(cartService.Count() == 0)

                return false;

            cartService.Empty();

            paymentService.ProcessPayment();

            return true;

        }

Applying Model-Based Testing for Fault-Injection in cloud services – Part II

Okay, so I have to admit I’m mixing things up a bit here. This week I wanted to go to a 2-service model, but I realized that would be jumping ahead of things. Instead I want to take the next steps in actually implementing the shopping cart service and the model interface to this service, as this has some interesting challenges.

First the service…

Shopping cart service

The shopping cart service is a Windows Azure WCF Service Web Role project. It implements a very crude interface. You can add an item to the cart, reset it (empty it), retrieve the number of stored items and proceed to checkout (which includes emptying the cart). The interface is:

    public interface IShoppingCart

    {

        /// <summary>

        /// Empties the shopping cart

        /// </summary>

        [OperationContract]

        void Reset();

        /// <summary>

        /// Adds the item with given name to the shopping cart

        /// </summary>

        /// <param name="item">Name of item to add</param>

        [OperationContract]

        void AddItem(string item);

        /// <summary>

        /// Returns the number of items currently in the cart

        /// </summary>

        /// <returns>Number of items in cart</returns>

        [OperationContract]

        int GetCount();

        /// <summary>

        /// Continues to payment input, and empties the shopping cart

        /// </summary>

        /// <returns>False if no items are in the cart</returns>

        [OperationContract]

        bool ProceedToCheckout();

    }

The service can be started from within Visual Studio where you can debug it, or you can generate an Azure ASP.NET Web Role that consumes it.

Writing tests against a service is piece-of-cake. You simply add a service reference to the test project and create a static instance of the service client, which you can then call. The adapter layer of our model based tests will simply call the appropriate service method for each action, with the exception of the “KillService” and “RestoreService” rules that are special.

The implementation of a shopping cart service can be found in the appendix [1]. 

These actions are a bit more tricky to implement...