Automatically assigned DDC number: 005115
Manually assigned DDC number: 005115

Number of references: 8

Title: Decoupling Synchronization from Logic for Efficient Symbolic Model Checking of Statecharts

Author:

Author:

Author:

Author:

Author:

Author:

Subject: William Chan,Richard J. Anderson,Paul Beame,David H. Jones,David Notkin,William E. Warner Decoupling Synchronization from Logic for Efficient Symbolic Model Checking of Statecharts

Description: Symbolic model checking is a powerful formal-verification technique for reactive systems. In this paper we address the problem of symbolic model checking for software specifications written as statecharts. We concentrate on how the synchronization of statecharts relates to the efficiency of model checking. We show that statecharts synchronized in an oblivious manner, such that the synchronization and the control logic are decoupled, tend to be easier for symbolic analysis. Thanks to this insight, the verification of some non-oblivious systems can be optimized by a simple, transparent modification to the model to separate the synchronization from the logic. The technique enabled the analysis of the statecharts model of a fault-tolerant electrical power distribution system developed by the Boeing Commercial Airplane Group. The results disclosed subtle modeling and logical flaws not found by simulation. Keywords Formal methods, verification, symbolic model checking, binary decision diag...

Contributor: The Pennsylvania State University CiteSeer Archives

Publisher: unknown

Date: 1998-09-15

Pubyear: 1998

Format: ps

Identifier: http://citeseer.ist.psu.edu/165981.html

Source: ftp://ftp.cs.washington.edu/tr/1998/09/UW-CSE-98-09-02.PS.Z

Language: en

Relation:

Relation:

Relation:

Relation:

Relation:

Relation:

Relation:

Relation:

Rights: unrestricted

Graph

<?xml version="1.0" encoding="UTF-8"?>

<references_metadata>

<rec ID="/517603.html" Type="article" CiteSeer_Book="Science of Computer Programming" CiteSeer_Volume="19" Title="The Esterel Synchronous Programming Language: Design, Semantics, Implementation,">

<identifier Org="ISBN:0387569227" Paper_ID="/517603.html" Extracted="0387569227" DDC="511.3/0285" Normalized_DDC="51130285" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:0821806807" Paper_ID="/517603.html" Extracted="0821806807" DDC="005.2/76" Normalized_DDC="005276" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:0849328241" Paper_ID="/517603.html" Extracted="0849328241" DDC="004.16" Normalized_DDC="00416" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:0897916972" Paper_ID="/517603.html" Extracted="0897916972" />

<identifier Org="ISBN:1558607021" Paper_ID="/517603.html" Extracted="1558607021" DDC="004.16" Normalized_DDC="00416" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:1841501220" Paper_ID="/517603.html" Extracted="1841501220" DDC="005.114" Normalized_DDC="005114" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540202234" Paper_ID="/517603.html" Extracted="3540202234" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540213139" Paper_ID="/517603.html" Extracted="3540213139" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540308814" Paper_ID="/517603.html" Extracted="3540308814" DDC="004.16" Normalized_DDC="00416" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540403256" Paper_ID="/517603.html" Extracted="3540403256" DDC="005.13" Normalized_DDC="00513" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540425411" Paper_ID="/517603.html" Extracted="3540425411" DDC="621.39/5" Normalized_DDC="621395" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540550925" Paper_ID="/517603.html" Extracted="3540550925" DDC="004/.33" Normalized_DDC="00433" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540575294" Paper_ID="/517603.html" Extracted="3540575294" DDC="004" Normalized_DDC="004" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540627812" Paper_ID="/517603.html" Extracted="3540627812" DDC="005.1/2" Normalized_DDC="00512" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540627901" Paper_ID="/517603.html" Extracted="3540627901" DDC="004.2/1" Normalized_DDC="00421" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540664599" Paper_ID="/517603.html" Extracted="3540664599" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540664629" Paper_ID="/517603.html" Extracted="3540664629" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540675302" Paper_ID="/517603.html" Extracted="3540675302" DDC="005.1/01/512" Normalized_DDC="005101512" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540712887" Paper_ID="/517603.html" Extracted="3540712887" />

</rec>

<rec ID="/311874.html" Type="article" CiteSeer_Book="ieeetc" CiteSeer_Volume="C35" Title="Graph-Based Algorithms for {B}oolean Function Manipulation," />

<rec ID="/19422.html" Type="inproceedings" CiteSeer_Book="Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science" CiteSeer_Volume="" Title="{S}ymbolic {M}odel {C}hecking: $10^{20}$ {S}tates and {B}eyond," />

<rec ID="/248596.html" Type="misc" CiteSeer_Book="" CiteSeer_Volume="" Title="Model checking large software specifications,">

<identifier Org="ISBN:0120121492" Paper_ID="/248596.html" Extracted="0120121492" />

<identifier Org="ISBN:0792373235" Paper_ID="/248596.html" Extracted="0792373235" DDC="005.1/4" Normalized_DDC="00514" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:1581130740" Paper_ID="/248596.html" Extracted="1581130740" />

<identifier Org="ISBN:354020461X" Paper_ID="/248596.html" Extracted="354020461X" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540210024" Paper_ID="/248596.html" Extracted="3540210024" DDC="005.1/4" Normalized_DDC="00514" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540408282" Paper_ID="/248596.html" Extracted="3540408282" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540410309" Paper_ID="/248596.html" Extracted="3540410309" DDC="005.2/76" Normalized_DDC="005276" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540418636" Paper_ID="/248596.html" Extracted="3540418636" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540418652" Paper_ID="/248596.html" Extracted="3540418652" DDC="004.2/11" Normalized_DDC="004211" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:354043738X" Paper_ID="/248596.html" Extracted="354043738X" DDC="005.1/0285" Normalized_DDC="00510285" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540439307" Paper_ID="/248596.html" Extracted="3540439307" DDC="005.115" Normalized_DDC="005115" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540627170" Paper_ID="/248596.html" Extracted="3540627170" />

<identifier Org="ISBN:3540631666" Paper_ID="/248596.html" Extracted="3540631666" DDC="004.24015113" Normalized_DDC="00424015113" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540650032" Paper_ID="/248596.html" Extracted="3540650032" DDC="004/.33" Normalized_DDC="00433" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540664882" Paper_ID="/248596.html" Extracted="3540664882" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540671021" Paper_ID="/248596.html" Extracted="3540671021" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540672826" Paper_ID="/248596.html" Extracted="3540672826" DDC="004.2/1" Normalized_DDC="00421" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540691472" Paper_ID="/248596.html" Extracted="3540691472" />

<identifier Org="ISBN:3540851135" Paper_ID="/248596.html" Extracted="3540851135" />

<identifier Org="ISBN:9812560947" Paper_ID="/248596.html" Extracted="9812560947" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.06666666666666667" />

</rec>

<rec ID="/543554.html" Type="article" CiteSeer_Book="Science of Computer Programming" CiteSeer_Volume="8" Title="Statecharts: {A} Visual Formalism for Complex Systems,">

<identifier Org="ISBN:0387984305" Paper_ID="/543554.html" Extracted="0387984305" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:0792384296" Paper_ID="/543554.html" Extracted="0792384296" DDC="005.1/17" Normalized_DDC="005117" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:1402052626" Paper_ID="/543554.html" Extracted="1402052626" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:1402062532" Paper_ID="/543554.html" Extracted="1402062532" />

<identifier Org="ISBN:1558607021" Paper_ID="/543554.html" Extracted="1558607021" DDC="004.16" Normalized_DDC="00416" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540203036" Paper_ID="/543554.html" Extracted="3540203036" DDC="005.3" Normalized_DDC="0053" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540253335" Paper_ID="/543554.html" Extracted="3540253335" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:354029189X" Paper_ID="/543554.html" Extracted="354029189X" DDC="004.6/2" Normalized_DDC="00462" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:354043738X" Paper_ID="/543554.html" Extracted="354043738X" DDC="005.1/0285" Normalized_DDC="00510285" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540442529" Paper_ID="/543554.html" Extracted="3540442529" DDC="004.2/4" Normalized_DDC="00424" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540545638" Paper_ID="/543554.html" Extracted="3540545638" DDC="006.3/3" Normalized_DDC="00633" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540550925" Paper_ID="/543554.html" Extracted="3540550925" DDC="004/.33" Normalized_DDC="00433" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540645829" Paper_ID="/543554.html" Extracted="3540645829" DDC="006.3" Normalized_DDC="0063" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540650032" Paper_ID="/543554.html" Extracted="3540650032" DDC="004/.33" Normalized_DDC="00433" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540654933" Paper_ID="/543554.html" Extracted="3540654933" DDC="004/.35" Normalized_DDC="00435" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540665889" Paper_ID="/543554.html" Extracted="3540665889" DDC="005.13/1" Normalized_DDC="005131" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540672613" Paper_ID="/543554.html" Extracted="3540672613" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.058823529411764705" />

<identifier Org="ISBN:3540708804" Paper_ID="/543554.html" Extracted="3540708804" />

<identifier Org="ISBN:3540728813" Paper_ID="/543554.html" Extracted="3540728813" />

<identifier Org="ISBN:3540752080" Paper_ID="/543554.html" Extracted="3540752080" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.058823529411764705" />

</rec>

<rec ID="/535995.html" Type="inproceedings" CiteSeer_Book="Computer Aided Verification" CiteSeer_Volume="" Title="Efficient Verification with {BDDs} using Implicitly Conjoined Invariants,">

<identifier Org="ISBN:0387569227" Paper_ID="/535995.html" Extracted="0387569227" DDC="511.3/0285" Normalized_DDC="51130285" Normalized_Weight="0.16666666666666666" />

<identifier Org="ISBN:0780318366" Paper_ID="/535995.html" Extracted="0780318366" />

<identifier Org="ISBN:0821805797" Paper_ID="/535995.html" Extracted="0821805797" DDC="005.2/76" Normalized_DDC="005276" Normalized_Weight="0.16666666666666666" />

<identifier Org="ISBN:0897916530" Paper_ID="/535995.html" Extracted="0897916530" />

<identifier Org="ISBN:1581130740" Paper_ID="/535995.html" Extracted="1581130740" />

<identifier Org="ISBN:3540206469" Paper_ID="/535995.html" Extracted="3540206469" DDC="006.3" Normalized_DDC="0063" Normalized_Weight="0.16666666666666666" />

<identifier Org="ISBN:354027829X" Paper_ID="/535995.html" Extracted="354027829X" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.16666666666666666" />

<identifier Org="ISBN:3540581790" Paper_ID="/535995.html" Extracted="3540581790" DDC="004.2/4/015113" Normalized_DDC="00424015113" Normalized_Weight="0.16666666666666666" />

<identifier Org="ISBN:3540607617" Paper_ID="/535995.html" Extracted="3540607617" DDC="005.2" Normalized_DDC="0052" Normalized_Weight="0.16666666666666666" />

<identifier Org="ISBN:3540698493" Paper_ID="/535995.html" Extracted="3540698493" />

<identifier Org="ISBN:3540733671" Paper_ID="/535995.html" Extracted="3540733671" />

</rec>

<rec ID="/106259.html" Type="misc" CiteSeer_Book="" CiteSeer_Volume="" Title="Efficient BDD algorithms for FSM synthesis and verification,">

<identifier Org="ISBN:0387259473" Paper_ID="/106259.html" Extracted="0387259473" DDC="005.115" Normalized_DDC="005115" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:0387301623" Paper_ID="/106259.html" Extracted="0387301623" DDC="518.103" Normalized_DDC="518103" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:0387341552" Paper_ID="/106259.html" Extracted="0387341552" DDC="621.3" Normalized_DDC="6213" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:0780372476" Paper_ID="/106259.html" Extracted="0780372476" />

<identifier Org="ISBN:0780391950" Paper_ID="/106259.html" Extracted="0780391950" />

<identifier Org="ISBN:1402045522" Paper_ID="/106259.html" Extracted="1402045522" />

<identifier Org="ISBN:1402072546" Paper_ID="/106259.html" Extracted="1402072546" DDC="621.39/5" Normalized_DDC="621395" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:1581130740" Paper_ID="/106259.html" Extracted="1581130740" />

<identifier Org="ISBN:3540232419" Paper_ID="/106259.html" Extracted="3540232419" DDC="005.1/1" Normalized_DDC="00511" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:354027829X" Paper_ID="/106259.html" Extracted="354027829X" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540412190" Paper_ID="/106259.html" Extracted="3540412190" DDC="621.39/2" Normalized_DDC="621392" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540423451" Paper_ID="/106259.html" Extracted="3540423451" DDC="004.24" Normalized_DDC="00424" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540425411" Paper_ID="/106259.html" Extracted="3540425411" DDC="621.39/5" Normalized_DDC="621395" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540433813" Paper_ID="/106259.html" Extracted="3540433813" DDC="511.3" Normalized_DDC="5113" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540439315" Paper_ID="/106259.html" Extracted="3540439315" DDC="006.3/33" Normalized_DDC="006333" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540439978" Paper_ID="/106259.html" Extracted="3540439978" DDC="004.24" Normalized_DDC="00424" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540662022" Paper_ID="/106259.html" Extracted="3540662022" DDC="004.24" Normalized_DDC="00424" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:3540664289" Paper_ID="/106259.html" Extracted="3540664289" DDC="006.3" Normalized_DDC="0063" Normalized_Weight="0.06666666666666667" />

<identifier Org="ISBN:9051994591" Paper_ID="/106259.html" Extracted="9051994591" DDC="004.2/1" Normalized_DDC="00421" Normalized_Weight="0.06666666666666667" />

</rec>

<rec ID="/304747.html" Type="inproceedings" CiteSeer_Book="Compass96 Eleventh Annual Conference on Computer Assurance" CiteSeer_Volume="" Title="Feasibility of Model Checking Software Requirements,">

<identifier Org="ISBN:0120121433" Paper_ID="/304747.html" Extracted="0120121433" />

<identifier Org="ISBN:0131469134" Paper_ID="/304747.html" Extracted="0131469134" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.1" />

<identifier Org="ISBN:0387953876" Paper_ID="/304747.html" Extracted="0387953876" DDC="005.8" Normalized_DDC="0058" Normalized_Weight="0.1" />

<identifier Org="ISBN:0612094146" Paper_ID="/304747.html" Extracted="0612094146" />

<identifier Org="ISBN:0780333918" Paper_ID="/304747.html" Extracted="0780333918" DDC="005.2/4" Normalized_DDC="00524" Normalized_Weight="0.1" />

<identifier Org="ISBN:0780339800" Paper_ID="/304747.html" Extracted="0780339800" />

<identifier Org="ISBN:0818677406" Paper_ID="/304747.html" Extracted="0818677406" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="0.1" />

<identifier Org="ISBN:1581130740" Paper_ID="/304747.html" Extracted="1581130740" />

<identifier Org="ISBN:3540417117" Paper_ID="/304747.html" Extracted="3540417117" DDC="658.5" Normalized_DDC="6585" Normalized_Weight="0.1" />

<identifier Org="ISBN:3540620346" Paper_ID="/304747.html" Extracted="3540620346" DDC="001.64" Normalized_DDC="00164" Normalized_Weight="0.1" />

<identifier Org="ISBN:354062600X" Paper_ID="/304747.html" Extracted="354062600X" DDC="004.1/9" Normalized_DDC="00419" Normalized_Weight="0.1" />

<identifier Org="ISBN:3540627901" Paper_ID="/304747.html" Extracted="3540627901" DDC="004.2/1" Normalized_DDC="00421" Normalized_Weight="0.1" />

<identifier Org="ISBN:3540631666" Paper_ID="/304747.html" Extracted="3540631666" DDC="004.24015113" Normalized_DDC="00424015113" Normalized_Weight="0.1" />

<identifier Org="ISBN:3540643567" Paper_ID="/304747.html" Extracted="3540643567" DDC="004.2/1" Normalized_DDC="00421" Normalized_Weight="0.1" />

<identifier Org="ISBN:3540929657" Paper_ID="/304747.html" Extracted="3540929657" />

</rec>

<rec ID="SELF" Type="SELF" CiteSeer_Book="SELF" CiteSeer_Volume="SELF" Title="Decoupling Synchronization from Logic for Efficient Symbolic Model Checking of Statecharts">

<identifier Org="ISBN:3540671021" Paper_ID="SELF" Extracted="3540671021" DDC="005.1" Normalized_DDC="0051" Normalized_Weight="1.0" />

</rec>

</references_metadata>