Some folks asked me to talk a bit about the history of Spec Explorer 2010, and how it relates to an older tool also called Spec Explorer which one can find here at Microsoft Research’s web page. So here is how the story goes.
The roots of the Spec Explorer technology, as known today, were laid out by a group of people in Microsoft Research around Yuri Gurevich – I was one of those, as was Margus Veanes, Wolfram Schulte, Lev Nachmanson, Colin Campbell, and very soon Nikolai Tillmann, one of my students back in times at TU Berlin. By 2001, when I joined this team, they were developing a specification language called AsmL, based on Yuri’s and others work on ASM (abstract state machines). The ASM approach is an operational, constructive (in contrast to axiomatic) approach to describe systems by means of evolving a system state iteratively by applying guarded state update rules. We thought AsmL was a beautiful and powerful language for the specification of systems, however, there were no obvious applications for it, so not many users were picking it up. While Microsoft Research is in general a foundational research institution and immediate pressure to bring things into practice doesn’t exist, some people in the group, including myself, were keen for success stories in practical application. So we searched for a killer application in applying formal specification and modeling. And that was soon identified to be in the testing space, as testing was and even more is today one of the most cost-intensive tasks in software development.
Bringing in some experience from my former work back in Germany on specification-based testing for safety critical embedded systems, we started out extending the existing AsmL compiler and runtime to be able to do state space exploration. This was technically relatively easy because AsmL already supported the concept of transactions, requiring the AsmL runtime to snapshot states and able to restore them for other execution paths, the core of state space exploration as it is done in Spec Explorer today. In a few weeks Nikolai Tillmann and I were able to “hack” together our first Model-Based testing tool, called AsmL-T, which was already surprisingly close to what Spec Explorer does today.
AsmL-T was relatively successful and we partnered with folks like Keith Stobie in Microsoft who promoted it for the application of testing of Indigo, Microsoft’s web service infrastructure. The application to testing was in fact so successful that at some point it became more important than the language behind it… In some sense, AsmL was just too much ahead of its time. The language was, in addition to the ASM approach, based on ideas from functional programming which Wolfram Schulte and I brought into it, which only years later should make it into mainstream languages like C# (catchword ‘LINQ’)…
So we decided to derive a ‘light-weight’ version of AsmL which we called Spec#, a language which made a career also for API contracts. Spec# was basically AsmL disguised in C# syntax. The AsmL compiler was augmented by a different parser to support the new frontend notation. The MBT tool was reengineered, and called ‘Spec Explorer’ for the first time -- more precisely, ‘Spec Explorer 2004’. The result of this work can be still downloaded today from the Microsoft Research site. Spec Explorer 2004 was applied with increasing success in Microsoft, having at some point a few hundred subscriptions on its internal distribution list. However, the breakthrough we expected never occurred. After around one year of availability, the number of users stagnated.
By 2005, the group at Microsoft Research responsible for Spec Explorer, now lead by Wolfram Schulte, revised its strategy around testing technology in general and Model-Based testing in particular. The project was split into two branches, one continuing the path of Model-Based testing, another focusing on white-box testing and leading to the Pex technology. One of the adoption problems identified for Model-Based testing was the lack of good educational material and so some folks of the former Spec Explorer team focused on writing a book about Model-Based testing, accompanied by a simplified open-source implementation of a tool, called NModel. The other part, including me, worked on a new version of the technology, set out to overcome some of the identified adoption problems of the technology. This team was soon augmented by Nico Kicillof from the University of Buenos Aires.
The problems identified and the proposed solutions have been described in the research paper Multi-Paradigmatic Model-Based Testing (published as an invited contribution to FATES/RV 2006). The main ones have being:
- Lack of adequate solutions to deal with the state explosion problem
- Use of custom specification languages instead of mainstream programming languages
- Missing support for scenario-oriented modeling (in contrast to state-oriented), and most particular, the composition of scenarios with state machines.
- Missing integration into state-of-the-art IDEs like Visual Studio
- Missing integration with existing test execution engines (like VSTT, NUnit, etc.)
The first prototype of the code base which today constitutes Spec Explorer 2010 was created in 2006, addressing the above problems by its unique new features, like model exploration based on CIL (thus enabling C# as an input notation), the Cord scripting language, a full integration into Visual Studio, and test suite code generation for VSTT. Various publications by Nico Kicillof and me document the foundations of this approach (this one about semantic foundations, this one about Cord).
Before the tool actually left the prototyping state something unexpected happened. Microsoft, in the course of its commitment to Open Protocols and Interoperability, launched a program to ensure the quality of protocol documentation by systematic testing of the protocol implementations based on the information found in the documents. The choice was made to apply in this big project, targeting more than 250 documents and test suites, Model-Based testing, and the tool of choice was the new version of Spec Explorer. So both Spec Explorer and I moved beginning of 2007 over into a new organization in the Windows Server Division, dedicated to protocol documentation testing using innovative testing technology. Soon, Keith Stobie as our test architect, and Nico Kicillof as our tools lead program manager joined the team as well. A development and testing team, based in Beijing was build up for Spec Explorer. Vendor teams in India and China applied Spec Explorer to test protocols based on a methodology developed by Keith, Nico, me, and many others in the team. Spec Explorer was applied on a large scale, in a project taking up more than 250 person years of testing. The choice of which test approach to use for each protocol – Model-Based or traditional – was left to the executing teams and their reviewers, and it resulted in the modeling approach being picked for about ½ the test suites. After 2 ½ years of testing, an average of 42% of efficiency improvement could be measured, using a very conservative empiric method, and having rather lay people working on the Model-Based approach.
The tools team in Beijing, under the leadership of Danpo Zhang, Ning Sun and Yiming Cao, did a fantastic job in stabilizing and extending the tool, and the test suite teams in India and China under the leadership of Dave MacDonald in applying it and providing feedback. At the point of this writing, I’m proud to be part of a team shipping a Model-Based testing solution, based on solid research of a nearly a decade, and validated for its feasibility in a large industry project with mission critical relevance! I hope you find this work useful as well. Enjoy!