{"id":187511,"date":"2012-02-29T00:00:00","date_gmt":"2012-03-27T07:37:20","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/msr-research-item\/a-system-for-programming-and-verifying-interacting-state-machines\/"},"modified":"2016-08-02T06:11:35","modified_gmt":"2016-08-02T13:11:35","slug":"a-system-for-programming-and-verifying-interacting-state-machines","status":"publish","type":"msr-video","link":"https:\/\/www.microsoft.com\/en-us\/research\/video\/a-system-for-programming-and-verifying-interacting-state-machines\/","title":{"rendered":"A system for programming and verifying interacting state machines"},"content":{"rendered":"<div class=\"asset-content\">\n<p>We present a new development environment for programs composed of interacting state machines.  It improves upon our previous work that enabled the formal development of the USB 3.0 device driver stack in Windows 8.  The new programming environment provides easy specification and visualization of state machines, comprehensive verification early in the design process, and efficient code generation.  We hope that these features would enable construction of reliable and correct  asynchronous software systems.  The verification capabilities of our system rest on two foundations&#8212;fast checking of syntactic properties via static analysis and potentially expensive checking of semantic properties via state exploration.  After giving an overview of the system, we will focus on our effort to improve the scalability of state exploration through compositional verification.  Our system allows the specification to be conjunctively decomposed into a collection of state machines.  Each specification machine provides a partial description of the interaction among the implementation machines and is verified separately, perhaps by using other specification machines as lemmas.  The compositional proof rule ensures soundness in spite of allowing circular use of lemmas.  In the talk, we will give details of the compositional proof methodology and its implementation using declarative programming with Formula and model checking with Zing.<\/p>\n<\/div>\n<p><!-- .asset-content --><\/p>\n","protected":false},"excerpt":{"rendered":"<p>We present a new development environment for programs composed of interacting state machines. It improves upon our previous work that enabled the formal development of the USB 3.0 device driver stack in Windows 8. The new programming environment provides easy specification and visualization of state machines, comprehensive verification early in the design process, and efficient [&hellip;]<\/p>\n","protected":false},"featured_media":196729,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"footnotes":""},"research-area":[],"msr-video-type":[206954],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-187511","msr-video","type-msr-video","status-publish","has-post-thumbnail","hentry","msr-video-type-microsoft-research-talks","msr-locale-en_us"],"msr_download_urls":"","msr_external_url":"https:\/\/youtu.be\/ZJZBQfsdf44","msr_secondary_video_url":"","msr_video_file":"","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/187511"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-video"}],"version-history":[{"count":0,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/187511\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/196729"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=187511"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=187511"},{"taxonomy":"msr-video-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video-type?post=187511"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=187511"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=187511"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=187511"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}