| Author | Title | Year | Journal/Proceedings | Reftype | DOI/URL | |
|---|---|---|---|---|---|---|
| Cabodi, G., Camurati, P., Garcia, L., Murciano, M., Nocco, S. & Quer, S. | Speeding up Model Checking by Exploiting Explicit and Hidden Verification Constraints | 2009 | DATE '09: Proceedings of the conference on Design, Automation and Test in Europe, pp. 1686-1691 | inproceedings | ||
| Abstract: Constraints represent a key component of state- of-the-art verification tools based on compositional approaches and assume–guarantee reasoning. In recent years, most of the research efforts on verification constraints have focused on defining formats and techniques to encode, or to synthesize, constraints starting from the specification of the design. In this paper, we analyze the impact of constraints on the performance of model checking tools, and we discuss how to effectively exploit them. We also introduce an approach to explicitly derive verification constraints hidden in the design and/or in the property under verification. Such constraints may simply come from true design constraints, embedded within the properties, or may be generated in the general effort to reduce or partition the state space. Experimental results show that, in both cases, we can reap benefits for the overall verification process in several hard-to-solve designs, where we obtain speed-ups of more than one order of magnitude. |
||||||
BibTeX:
@inproceedings{Cabodi09Speeding,
author = {G. Cabodi and P. Camurati and L. Garcia and M. Murciano and S. Nocco and S. Quer},
title = {Speeding up Model Checking by Exploiting Explicit and Hidden Verification Constraints},
booktitle = {DATE '09: Proceedings of the conference on Design, Automation and Test in Europe},
year = {2009},
pages = {1686-1691}
}
|
||||||
| Feng, Y., Veeramani, A., Kanagasabai, R. & Rho, S. | Automatic Service Composition via Model Checking | 2011 | Services Computing Conference (APSCC), 2011 IEEE Asia-Pacific, pp. 477 -482 | inproceedings | DOI | |
| Abstract: Web service composition is the process of constructing a set of Web services which, when invoked with some user input in a particular order, can produce the output to the user's requirements. This paper proposes a novel model checking based approach for automated service composition. Modeling services as a set of interleaved processes in a class of process algebra, we formulate service composition as model checking asserted on a specific type of property on the model. We show that, under this formulation, correct composition workflows can be constructed from the counter-examples provided by model checking. With a case study on online hotel booking services, we demonstrate that the proposed approach can support directed a cyclic composition graphs and the generated composition graphs are automatically verified. | ||||||
BibTeX:
@inproceedings{6128043,
author = {Yuzhang Feng and Veeramani, A. and Kanagasabai, R. and Seungmin Rho},
title = {Automatic Service Composition via Model Checking},
booktitle = {Services Computing Conference (APSCC), 2011 IEEE Asia-Pacific},
year = {2011},
pages = {477 -482},
doi = {http://dx.doi.org/10.1109/APSCC.2011.54}
}
|
||||||
| Lomuscio, A., Strulo, B., Walker, N. & Wu, P. Jin Dong and Huibiao Zhu (Ed.) | Assume-Guarantee Reasoning with Local Specifications | 2010 | Vol. 6447Formal Methods and Software Engineering, pp. 204-219 |
incollection | URL | |
| Abstract: We investigate assume-guarantee reasoning for global specifications consisting of conjunctions of local specifications. We present a sound and complete assume-guarantee rule that permits reasoning about individual modules for local specifications and draws conclusions on global specifications. We illustrate our approach with an example from the field of network congestion control, where different agents are responsible for controlling packet flow across a shared infrastructure. In this context, we derive an assume-guarantee rule for system stability, and show that this rule is valuable to reason about any number of agents, any initial flow configuration, and any topology of bounded degree. | ||||||
BibTeX:
@incollection{springerlink:10.1007/978-3-642-16901-4_15,
author = {Lomuscio, Alessio and Strulo, Ben and Walker, Nigel and Wu, Peng},
title = {Assume-Guarantee Reasoning with Local Specifications},
booktitle = {Formal Methods and Software Engineering},
publisher = {Springer Berlin / Heidelberg},
year = {2010},
volume = {6447},
pages = {204-219},
note = {10.1007/978-3-642-16901-4_15},
url = {http://dx.doi.org/10.1007/978-3-642-16901-4_15}
}
|
||||||
| Tripakis, S., Andrade, H., Ghosal, A., Limaye, R., Ravindran, K., Wang, G., Yang, G., Kormerup, J. & Wong, I. | Correct and non-defensive glue design using abstract models | 2011 | Proceedings of the seventh IEEE/ACM/IFIP international conference on Hardware/software codesign and system synthesis, pp. 59-68 | inproceedings | DOI URL | |
| Abstract: Current hardware design practice often relies on integration of components, some of which may be IP or legacy blocks. While integration eases design by allowing modularization and component reuse, it is still done in a mostly ad hoc manner. Designers work with descriptions of components that are either informal or incomplete (e.g., documents in English, structural but non-behavioral specifications in IP-XACT) or too low-level (e.g., HDL code), and have little to no automatic support for stitching the components together. Providing such support is the glue design problem. This paper addresses this problem using a model-based approach. The key idea is to use high-level models, such as dataflow graphs, that enable efficient automated analysis. The analysis can be used to derive performance properties of the system (e.g., component compatibility, throughput, etc.), optimize resource usage (e.g., buffer sizes), and even synthesize low-level code (e.g., control logic). However, these models are only abstractions of the real system, and often omit critical information. As a result, the analysis outcomes may be defensive (e.g., buffers that are too big) or even incorrect (e.g., buffers that are too small). The paper examines these situations and proposes a correct and non-defensive design methodology that employs the right models to explore accurate performance and resource trade-offs. |
||||||
BibTeX:
@inproceedings{Tripakis201,
author = {Tripakis, Stavros and Andrade, Hugo and Ghosal, Arkadeb and Limaye, Rhishikesh and Ravindran, Kaushik and Wang, Guoqiang and Yang, Guang and Kormerup, Jacob and Wong, Ian},
title = {Correct and non-defensive glue design using abstract models},
booktitle = {Proceedings of the seventh IEEE/ACM/IFIP international conference on Hardware/software codesign and system synthesis},
publisher = {ACM},
year = {2011},
pages = {59--68},
url = {http://doi.acm.org/10.1145/2039370.2039382},
doi = {http://doi.acm.org/10.1145/2039370.2039382}
}
|
||||||
| Zheng, H., Yao, H. & Yoneda, T. | Modular Model Checking of Large Asynchronous Designs with Efficient Abstraction Refinement | 2010 | Computers, IEEE Transactions on Vol. 59(4), pp. 561 -573 |
article | DOI | |
| Abstract: Divide-and-conquer is essential to address state explosion in model checking. Verifying each individual component in a system, in isolation, efficiently requires an appropriate context, which traditionally is obtained by hand. This paper presents an efficient modular model checking approach for asynchronous design verification. It is equipped with a novel abstraction refinement method that can refine a component abstraction to be accurate enough for successful verification. It is fully automated, and eliminates the need of finding an accurate context when verifying each individual component, although such a context is still highly desirable. This method is also enhanced with additional state space reduction techniques. The experiments on several nontrivial asynchronous designs show that this method efficiently removes impossible behaviors from each component including ones violating correctness requirements. | ||||||
BibTeX:
@article{5374376,
author = {Hao Zheng and Haiqiong Yao and Yoneda, T.},
title = {Modular Model Checking of Large Asynchronous Designs with Efficient Abstraction Refinement},
journal = {Computers, IEEE Transactions on},
year = {2010},
volume = {59},
number = {4},
pages = {561 -573},
doi = {http://dx.doi.org/10.1109/TC.2009.187}
}
|
||||||
Created by JabRef on 01/03/2012.