{"id":170116,"date":"2008-12-10T17:24:32","date_gmt":"2008-12-10T17:24:32","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/model-based-testing-with-specexplorer\/"},"modified":"2017-05-31T15:26:57","modified_gmt":"2017-05-31T22:26:57","slug":"model-based-testing-with-specexplorer","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/model-based-testing-with-specexplorer\/","title":{"rendered":"Model-based Testing with SpecExplorer"},"content":{"rendered":"<p><img loading=\"lazy\" decoding=\"async\" class=\"alignleft\" src=\"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/model-based-testing-with-specexplorer-2.gif\" width=\"67\" height=\"67\" \/>Spec Explorer is a software development tool for advanced model-based specification and conformance testing.<\/p>\n<p>&nbsp;<\/p>\n<h2>New Version of Spec Explorer as an extension to Visual Studio is now available: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/visualstudiogallery.msdn.microsoft.com\/271d0904-f178-4ce9-956b-d9bfa4902745\/\">Spec Explorer 2010<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/h2>\n<h2>What are the core ideas behind Spec Explorer?<\/h2>\n<ul>\n<li>Encode a system&#8217;s intended behavior (its specification) in machine-executable form (as a &#8220;model program&#8221;). The model program typically does much less than the implementation; it does just enough to capture the relevant states of the system and show the constraints that a correct implementation must follow. The goal is to specify from a chosen viewpoint what the system must do, what it may do and what it must not do.<\/li>\n<li>Explore the possible runs of the specification-program as a way to systematically generate test suites.<\/li>\n<li>Compare the behavior of the model program to the system&#8217;s implementation in each of the scenarios discovered by algorithmic exploration.\u00a0\u00a0Discrepancies between actual and expected results are called conformance failures.<\/li>\n<\/ul>\n<h2>What\u00a0is a conformance error?<\/h2>\n<p>A confrmance error may indicate any of the following:<\/p>\n<ul>\n<li>Implementation Bug. A code defect in the implementation under test [IUT].<\/li>\n<li>Modeling error. A code defect in the model program itself.<\/li>\n<li>Specification error. A mistake or ambiguity in the system&#8217;s specification (in other words, a misrepresentation of the intended system behavior).<\/li>\n<li>Design error. A logical inconsistency in the system&#8217;s intended behavior.<\/li>\n<\/ul>\n<h2>What components do belong to Spec Explorer?<\/h2>\n<p>Spec Explorer 2004 consists of:<\/p>\n<ul>\n<li>The software modeling languages <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/project\/spec\/\">Spec#<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> and <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/project\/asml-abstract-state-machine-language\/\" target=\"_self\">AsmL<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>.<\/li>\n<li>An explicit-state model checker, which allows the user to search the (possibly infinite) space of all possible sequences of method invocations that 1) do not violate the pre- and postconditions and invariants of the system&#8217;s contracts and 2) are relevant to a user-specified set of test properties.<\/li>\n<li>A traversal engine, which unwinds the resulting finite state machine to produce behavioral tests that cover all explored transitions.<\/li>\n<li>A binding mechanism allows users to associate actions of the model with methods of an implementation written .NET language. Both managed and unmanaged implementations may be tested if the .NET interop features are used.<\/li>\n<li>A conformance checker that executes the generated behavioral tests. Alternatively, Spec Explorer supports an \u201con-the-fly\u201d mode where test derivation (via model checking and traversal) and conformance checking of the implementation occur together.<\/li>\n<\/ul>\n<h2>What is the Future of \u00a0Spec Explorer?<\/h2>\n<p><strong>The next generation of Spec Explorer is now available from<\/strong>: <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/visualstudiogallery.msdn.microsoft.com\/271d0904-f178-4ce9-956b-d9bfa4902745\/\">Spec Explorer 2010<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/p>\n<p>This is the\u00a0original\u00a0research version: <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/download\/spec-explorer\/\" target=\"_new\">Spec Explorer (version 1.0.9520).<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/p>\n<p>You can also use <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/www.codeplex.com\/NModel\" target=\"_self\">NModel<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><b>, which is<\/b>\u00a0is an <em>open source<\/em>\u00a0model-based analysis and testing framework for model programs written in C#. It is explained and used in the book <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"http:\/\/staff.washington.edu\/jon\/modeling-book\/\">Model-based Software Testing and Analysis with C#<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Spec Explorer is a software development tool for advanced model-based specification and conformance testing. &nbsp; New Version of Spec Explorer as an extension to Visual Studio is now available: Spec Explorer 2010 What are the core ideas behind Spec Explorer? Encode a system&#8217;s intended behavior (its specification) in machine-executable form (as a &#8220;model program&#8221;). The [&hellip;]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"footnotes":""},"research-area":[13560],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-170116","msr-project","type-msr-project","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2008-12-10","related-publications":[155872,156792,155885,156010,152798,156074,155822,156112,155833,156113,155852,156115,155858,156117,155860,156118,155862,156119,155868,156121],"related-downloads":[235001],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","value":"margus","display_name":"Margus Veanes","author_link":"<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/people\/margus\/\" aria-label=\"Visit the profile page for Margus Veanes\">Margus Veanes<\/a>","is_active":false,"user_id":32806,"last_first":"Veanes, Margus","people_section":0,"alias":"margus"}],"msr_research_lab":[199565],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170116"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":2,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170116\/revisions"}],"predecessor-version":[{"id":387908,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170116\/revisions\/387908"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=170116"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=170116"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=170116"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=170116"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=170116"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}