{"id":156121,"date":"2003-01-01T00:00:00","date_gmt":"2003-01-01T00:00:00","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/msr-research-item\/combined-algorithm-for-approximating-a-finite-state-abstraction-of-a-large-system\/"},"modified":"2018-10-16T20:14:40","modified_gmt":"2018-10-17T03:14:40","slug":"combined-algorithm-for-approximating-a-finite-state-abstraction-of-a-large-system","status":"publish","type":"msr-research-item","link":"https:\/\/www.microsoft.com\/en-us\/research\/publication\/combined-algorithm-for-approximating-a-finite-state-abstraction-of-a-large-system\/","title":{"rendered":"Combined Algorithm for Approximating a Finite State Abstraction of a Large System"},"content":{"rendered":"<div class=\"asset-content\">\n<p>We study the problem of abstracting a finite state machine (FSM) from a given software system whose operational behavior is described by an abstract state machine (ASM). ASMs are typically infinite state systems and the problem of extracting a finite abstraction, the true FSM, from an ASM with respect to a given abstraction function is in general undecidable. To approximate the true FSM we utilize the two key features of ASMs, that they are executable and have precise mathematical semantics that allows for a symbolic representation of the overall system behavior. On one hand, executability of ASMs is exploited for true computation path exploration; this yields an under-approximation of the true FSM. On the other hand, the symbolic representation of the system behavior enables us to use theorem proving to exclude impossible computation paths; this yields an over-approximation of the true FSM. In this paper we discuss an algorithm that combines both into a unified approach.<\/p>\n<\/div>\n<p><!-- .asset-content --><\/p>\n","protected":false},"excerpt":{"rendered":"<p>We study the problem of abstracting a finite state machine (FSM) from a given software system whose operational behavior is described by an abstract state machine (ASM). ASMs are typically infinite state systems and the problem of extracting a finite abstraction, the true FSM, from an ASM with respect to a given abstraction function is [&hellip;]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr-author-ordering":null,"msr_publishername":"","msr_publisher_other":"","msr_booktitle":"ICSE 2003\/Scenarios Workshop","msr_chapter":"","msr_edition":"ICSE 2003\/Scenarios Workshop","msr_editors":"","msr_how_published":"","msr_isbn":"","msr_issue":"","msr_journal":"","msr_number":"","msr_organization":"","msr_pages_string":"86-91","msr_page_range_start":"86","msr_page_range_end":"91","msr_series":"","msr_volume":"","msr_copyright":"","msr_conference_name":"ICSE 2003\/Scenarios Workshop","msr_doi":"","msr_arxiv_id":"","msr_s2_paper_id":"","msr_mag_id":"","msr_pubmed_id":"","msr_other_authors":"Rostislav Yavorsky","msr_other_contributors":"","msr_speaker":"","msr_award":"","msr_affiliation":"","msr_institution":"","msr_host":"","msr_version":"","msr_duration":"","msr_original_fields_of_study":"","msr_release_tracker_id":"","msr_s2_match_type":"","msr_citation_count_updated":"","msr_published_date":"2003-01-01","msr_highlight_text":"","msr_notes":"","msr_longbiography":"","msr_publicationurl":"","msr_external_url":"","msr_secondary_video_url":"","msr_conference_url":"","msr_journal_url":"","msr_s2_pdf_url":"","msr_year":2003,"msr_citation_count":0,"msr_influential_citations":0,"msr_reference_count":0,"msr_s2_match_confidence":0,"msr_microsoftintellectualproperty":true,"msr_s2_open_access":false,"msr_s2_author_ids":[],"msr_pub_ids":[],"msr_hide_image_in_river":0,"footnotes":""},"msr-research-highlight":[],"research-area":[13560],"msr-publication-type":[193716],"msr-publisher":[],"msr-focus-area":[],"msr-locale":[268875],"msr-post-option":[],"msr-field-of-study":[],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-156121","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us"],"msr_publishername":"","msr_edition":"ICSE 2003\/Scenarios Workshop","msr_affiliation":"","msr_published_date":"2003-01-01","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"ICSE 2003\/Scenarios Workshop","msr_pages_string":"86-91","msr_chapter":"","msr_isbn":"","msr_journal":"","msr_volume":"","msr_number":"","msr_editors":"","msr_series":"","msr_issue":"","msr_organization":"","msr_how_published":"","msr_notes":"","msr_highlight_text":"","msr_release_tracker_id":"","msr_original_fields_of_study":"","msr_download_urls":"","msr_external_url":"","msr_secondary_video_url":"","msr_longbiography":"","msr_microsoftintellectualproperty":1,"msr_main_download":"210324","msr_publicationurl":"","msr_doi":"","msr_publication_uploader":[{"type":"file","title":"scesm03.pdf","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/scesm03.pdf","id":210324,"label_id":0}],"msr_related_uploader":"","msr_citation_count":0,"msr_citation_count_updated":"","msr_s2_paper_id":"","msr_influential_citations":0,"msr_reference_count":0,"msr_arxiv_id":"","msr_s2_author_ids":[],"msr_s2_open_access":false,"msr_s2_pdf_url":null,"msr_attachments":[{"id":210324,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/scesm03.pdf"}],"msr-author-ordering":[{"type":"text","value":"Rostislav Yavorsky","user_id":0,"rest_url":false},{"type":"user_nicename","value":"margus","user_id":32806,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=margus"}],"msr_impact_theme":[],"msr_research_lab":[],"msr_event":[],"msr_group":[],"msr_project":[170116,169448],"publication":[],"video":[],"msr-tool":[],"msr_publication_type":"inproceedings","related_content":{"projects":[{"ID":170116,"post_title":"Model-based Testing with SpecExplorer","post_name":"model-based-testing-with-specexplorer","post_type":"msr-project","post_date":"2008-12-10 17:24:32","post_modified":"2017-05-31 15:26:57","post_status":"publish","permalink":"https:\/\/www.microsoft.com\/en-us\/research\/project\/model-based-testing-with-specexplorer\/","post_excerpt":"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's intended behavior (its specification) in machine-executable form (as a \"model program\"). The model program typically does much less than the implementation; it does just enough to capture the relevant states of the&hellip;","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170116"}]}},{"ID":169448,"post_title":"AsmL: Abstract State Machine Language","post_name":"asml-abstract-state-machine-language","post_type":"msr-project","post_date":"2001-11-02 14:38:33","post_modified":"2017-06-01 14:57:37","post_status":"publish","permalink":"https:\/\/www.microsoft.com\/en-us\/research\/project\/asml-abstract-state-machine-language\/","post_excerpt":"AsmL is an industrial-strength executable specification language. It can be used at any stage of the programming process: design, coding, or testing. It is fully integrated into the Microsoft .NET environment: AsmL models can interoperate with any other .NET assembly, no matter what source language it is written in. AsmL uses XML and Word for literate specifications. What is AsmL? AsmL is the Abstract State Machine Language. The FSE group develops AsmL. It is an&hellip;","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/169448"}]}}]},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/156121","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-research-item"}],"version-history":[{"count":1,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/156121\/revisions"}],"predecessor-version":[{"id":525081,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/156121\/revisions\/525081"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=156121"}],"wp:term":[{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=156121"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=156121"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=156121"},{"taxonomy":"msr-publisher","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publisher?post=156121"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=156121"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=156121"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=156121"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=156121"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=156121"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=156121"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=156121"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=156121"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}