Name
Abstract | ||
|---|---|---|
We propose a model for modular synchronous systems with combinationM dependencies and define consistency using this model. We then show how to derive this model from a modular specification where individual modules are specified as Kripke Structures and give an Mgorithm to check the system for consistency. We have implemented this Mgorithm symbolicMly using BDDs in a tool, SpecCheck. We have used this tool to check an example bus protocol derived from an industrial specification. The counterexamples obtained for this protocol highlight the need for consistency checking. |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1007/3-540-40922-X_30 | FMCAD |
Keywords | Field | DocType |
modular synchronous systems,modular synchronous system,consistency checking,individual module,industrial specification,modular specification,kripke structures,example bus protocol,combinationm dependency,mgorithm symbolicmly | Kripke structure,Sequential consistency,Computer science,Real-time computing,Theoretical computer science,Linear temporal logic,Modular design,Consistency model,Counterexample,Modular specification | Conference |
Volume | ISSN | ISBN |
1954 | 0302-9743 | 3-540-41219-0 |
Citations | PageRank | References |
5 | 0.96 | 7 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Randal E. Bryant | 1 | 9204 | 1194.64 |
| Pankay Chauhan | 2 | 16 | 1.81 |
| Edmund M. Clarke | 3 | 20645 | 2418.32 |
| Amit Goel | 4 | 279 | 21.29 |