Spec Explorer

Last updated
Spec Explorer
Developer(s) Microsoft
Stable release
2010 Release 3.5.3146.0 / July 8, 2013;10 years ago (2013-07-08)
Operating system Microsoft Windows
Type Model-Based Testing tool

Spec Explorer [1] is a Model-Based Testing (MBT [2] [3] ) tool from Microsoft. It extends the Visual Studio Integrated Development Environment with the ability to define a model describing the expected behavior of a software system. From these models, the tool can generate tests automatically for execution within Visual Studio's own testing framework, or many other unit testing frameworks.

The concepts behind Spec Explorer and the tool itself have been described in several publications [4] [5] [6] [7] [8] [9] [10] [11] [12] [13] and presented in multiple academic and industry events. [14] [15] [16] [17]

The latest version can be downloaded from Visual Studio Gallery. [18] Technical information can be found in the Microsoft documentation. [19] Community and engineering team support can be obtained through the Spec Explorer Forum, [20] while the Spec Explorer Team Blog [21] provides detailed articles and guidance. [22]

Related Research Articles

Erich Gamma is a Swiss computer scientist and one of the four co-authors of the software engineering textbook, Design Patterns: Elements of Reusable Object-Oriented Software.

The World Wide Web has become a major delivery platform for a variety of complex and sophisticated enterprise applications in several domains. In addition to their inherent multifaceted functionality, these Web applications exhibit complex behaviour and place some unique demands on their usability, performance, security, and ability to grow and evolve. However, a vast majority of these applications continue to be developed in an ad hoc way, contributing to problems of usability, maintainability, quality and reliability. While Web development can benefit from established practices from other related disciplines, it has certain distinguishing characteristics that demand special considerations. In recent years, there have been developments towards addressing these considerations.

<span class="mw-page-title-main">Model-based testing</span>

Model-based testing is an application of model-based design for designing and optionally also executing artifacts to perform software testing or system testing. Models can be used to represent the desired behavior of a system under test (SUT), or to represent testing strategies and a test environment. The picture on the right depicts the former approach.

In programming and software development, fuzzing or fuzz testing is an automated software testing technique that involves providing invalid, unexpected, or random data as inputs to a computer program. The program is then monitored for exceptions such as crashes, failing built-in code assertions, or potential memory leaks. Typically, fuzzers are used to test programs that take structured inputs. This structure is specified, e.g., in a file format or protocol and distinguishes valid from invalid input. An effective fuzzer generates semi-valid inputs that are "valid enough" in that they are not directly rejected by the parser, but do create unexpected behaviors deeper in the program and are "invalid enough" to expose corner cases that have not been properly dealt with.

In computer science, an abstract state machine (ASM) is a state machine operating on states that are arbitrary data structures.

<span class="mw-page-title-main">Professional Developers Conference</span> Former series of conferences by Microsoft

Microsoft's Professional Developers Conference (PDC) was a series of conferences for software developers; the conference was held infrequently to coincide with beta releases of the Windows operating system, and showcased topics of interest to those developing hardware and software for the new version of Windows.

The Windows Driver Kit (WDK) is a software toolset from Microsoft that enables the development of device drivers for the Microsoft Windows platform. It includes documentation, samples, build environments, and tools for driver developers. A complete toolset for driver development also need the following: a compiler Visual Studio, Windows SDK, and Windows HLK.

Abstract State Machine Language (AsmL) is a programming language based on abstract state machines developed by Microsoft. AsmL is a functional language.

Rigi is an interactive graph editor tool for software reverse engineering using the white box method, i.e. necessitating source code, thus it is mainly aimed at program comprehension. Rigi is distributed by its main author, Hausi A. Müller and the Rigi research group at the University of Victoria.

The Toolkit for Conceptual Modeling (TCM) is a collection of software tools to present specifications of software systems in the form of diagrams, tables, trees, and the like. TCM offers editors for techniques used in Structured Analysis as well as editors for object-oriented (UML) techniques. For some of the behavior specification techniques, an interface to model checkers is offered. More in particular, TCM contains the following editors.

James D. McCaffrey is an American research software engineer at Microsoft Research known for his contributions to machine learning, combinatorics, and software test automation.

MERODE is an Object Oriented Enterprise Modeling method developed at KU Leuven (Belgium). Its name is the abbreviation of Model driven, Existence dependency Relation, Object oriented DEvelopment. MERODE is a method for creating domain models as basis for building information systems making use of two prominent UML diagramming techniques - class diagram and state diagrams. Starting from a high-level PIM allows removing or hiding details irrelevant for a conceptual modelling view which makes the approach easier to understand. The method is grounded in process algebra, which enables mathematical reasoning on models. Thanks to this, models can be checked for internal consistency and mutual completeness, i.e. inter/intra model consistency and syntactical quality. The automated reasoning also caters for autocomplete functionality, which allows creating correct models faster.

<span class="mw-page-title-main">Visual Studio</span> Code editor and IDE

Visual Studio is an integrated development environment (IDE) from Microsoft. It is used to develop computer programs including websites, web apps, web services and mobile apps. Visual Studio uses Microsoft software development platforms such as Windows API, Windows Forms, Windows Presentation Foundation, Windows Store and Microsoft Silverlight. It can produce both native code and managed code.

Visual Studio Tools for Applications (VSTA) is a set of tools that independent software vendors (ISVs) can use to build customization abilities into their applications for both automation and extensibility. Those customization abilities can be used by end-users to tailor the ISV's application within a managed extensibility environment just like Visual Basic for Applications.

<span class="mw-page-title-main">Yuri Gurevich</span> American computer scientist

Yuri Gurevich, Professor Emeritus at the University of Michigan, is an American computer scientist and mathematician and the inventor of abstract state machines.

<span class="mw-page-title-main">Behavior tree</span>

Behavior trees are a formal, graphical modelling language used primarily in systems and software engineering. Behavior trees employ a well-defined notation to unambiguously represent the hundreds or even thousands of natural language requirements that are typically used to express the stakeholder needs for a large-scale software-integrated system.

ISP is a tool for the formal verification of MPI programs developed within the School of Computing at the University of Utah. Like model checkers, such as SPIN, ISP verifies the complete state space of a system for a set of safety properties. However, unlike model checkers, ISP performs code level verification. This means that the tool verifies all relevant interleavings of a concurrent program by replaying the actual program code without building verification models. This idea was pioneered in a number of tools, notably by Godefroid, in his VeriSoft tool. Other recent tools of this genre include the Java Pathfinder, Microsoft's CHESS tool, and MODIST. Relevant interleavings are computed using a customized dynamic partial order reduction algorithm called POE.

WinWrap Basic (WWB) by Polar Engineering, Inc. is a third-party macro language based on Visual Basic used with programmes of various types which its vendor touts as an alternative to ActiveX, Visual Basic for Applications, and VSTA for this purpose. The WWB software package is used in conjunction with Microsoft development tools including Visual Studio, Visual Studio.NET, and the ActiveX scripting engines. The default file extension for programmes written in this language is .wwb.

Concolic testing is a hybrid software verification technique that performs symbolic execution, a classical technique that treats program variables as symbolic variables, along a concrete execution path. Symbolic execution is used in conjunction with an automated theorem prover or constraint solver based on constraint logic programming to generate new concrete inputs with the aim of maximizing code coverage. Its main focus is finding bugs in real-world software, rather than demonstrating program correctness.

<span class="mw-page-title-main">ML.NET</span> Machine learning library

ML.NET is a free software machine learning library for the C# and F# programming languages. It also supports Python models when used together with NimbusML. The preview release of ML.NET included transforms for feature engineering like n-gram creation, and learners to handle binary classification, multi-class classification, and regression tasks. Additional ML tasks like anomaly detection and recommendation systems have since been added, and other approaches like deep learning will be included in future versions.

References

  1. ↑ "Spec Explorer Visual Studio Power Tool".
  2. ↑ "Model-Based Testing Gold Practice".
  3. ↑ "Harry Robinson's Model-Based Testing Home Page". Archived from the original on 2009-10-27.
  4. ↑ Mark Utting and Bruno Legeard. Practical Model-Based Testing. Morgan-Kaufmann, 2007.
  5. ↑ Wolfgang Grieskamp. Multi-Paradigmatic Model-Based Testing. Invited talk in Klaus Havelund and Manuel Nunez and Grigore Rosu and Burkhart Wolff, FATES/RV, LNCS 4262, 2006.
  6. ↑ Colin Campbell, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, and Margus Veanes. Model-based testing of object-oriented reactive systems with Spec Explorer. Formal Methods and Testing 2008, LNCS 4949, Springer, 2008, pp. 39-76.
  7. ↑ Wolfgang Grieskamp, Yuri Gurevich, Wolfram Schulte, and Margus Veanes. Generating finite state machines from abstract state machines. In Proceedings of ISSTA’02, volume 27 of Software Engineering Notes, pages 112–122. ACM, 2002.
  8. ↑ Keith Stobie. Model based testing in practice at Microsoft. In Proceedings of the Workshop on Model Based Testing (MBT 2004), volume 111 of Electronic Notes in Theoretical Computer Science. Elsevier, 2004.
  9. ↑ Wolfgang Grieskamp, Nicolas Kicillof, Nikolai Tillmann. Action Machines: a Framework for Encoding and Composing Partial Behaviors. International Journal of Software Engineering and Knowledge Engineering 16(5): 705-726, 2006.
  10. ↑ Wolfgang Grieskamp, Dave MacDonald, Nicolas Kicillof, Alok Nandan, Keith Stobie, and Fred Wurden. Model-Based Quality Assurance of Windows Protocol Documentation. In Proceedings of the 1st IEEE International Conference on Software Testing (ICST 2008), Lillihammer, Norway, April 2008.
  11. ↑ Yuri Gurevich. Evolving Algebras 1993: Lipari Guide. In E. Boerger, editor, Specification and Validation Methods, pages 9–36. Oxford University Press, 1995.
  12. ↑ R. Alur, T. A. Henzinger, O. Kupferman, M. Y. Vardi: Alternating Refinement Relations. In Proceedings of the Ninth International Conference on Concurrency Theory (CONCUR), LNCS 1466, Springer, 1998.
  13. ↑ Wolfgang Grieskamp and Nicolas Kicillof. A schema language for coordinating construction and composition of partial behaviors. In Proceedings of the 28th International Conference on Software Engineering & Co-Located Workshops – 5th International Workshop on Scenarios and State Machines. ACM, May 2006.
  14. ↑ "Formal Approaches to Testing and Runtime Verification 2006".
  15. ↑ "IEEE International Conference on Software Testing Verification and Validation 2008".
  16. ↑ "International Conference on Quality Software 2008".
  17. ↑ "Storage Developer Conference".
  18. ↑ "Spec Explorer 2010 Visual Studio Power Tool".
  19. ↑ "Spec Explorer @ the Microsoft Developer Network".
  20. ↑ "The Model-Based Testing with Spec Explorer Forum".
  21. ↑ "The Spec Explorer Team Blog".
  22. ↑ https://softwareengineer1.blogspot.com/2019/02/spec-explorer-lives-getting-spec.html Spec Explorer 2010 supported on VS2013, VS2015, VS2017
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.