CADP 2011: A toolbox for the construction and analysis of distributed processes

被引：153
作者：
Garavel H. [1 ]
Lang F. [1 ]
Mateescu R. [1 ]
Serwe W. [1 ]
机构：
[1] INRIA/Laboratoire d'Informatique de Grenoble, VASY Team, 655, Avenue de l'Europe
来源：
International Journal on Software Tools for Technology Transfer | 2013年 / 15卷 / 02期
关键词：
Asynchronous concurrency; Equivalence checking; Formal methods; Model checking; Performance evaluation; Process calculus; Verification;
D O I：
10.1007/s10009-012-0244-z
中图分类号：
学科分类号：
摘要：
CADP (Construction and Analysis of Distributed Processes) is a comprehensive software toolbox that implements the results of concurrency theory. Started in the mid-1980s, CADP has been continuously developed by adding new tools and enhancing existing ones. Today, CADP benefits from a worldwide user community, both in academia and industry. This paper presents the latest release, CADP 2011, which is the result of a considerable development effort spanning the last five years. The paper first describes the theoretical principles and the modular architecture of CADP, which has inspired several other recent model checkers. The paper then reviews the main features of CADP 2011, including compilers for various formal specification languages, equivalence checkers, model checkers, compositional verification tools, performance evaluation tools, and parallel verification tools running on clusters and grids. Finally, the paper surveys some significant case studies. © 2012 Springer-Verlag.
引用
收藏
页码：89 / 107
页数：18
相关论文
共 128 条
[1]  
Andersen, H.R., Model checking and boolean graphs (1994) Theor. Comput. Sci., 126 (1), pp. 3-30
[2]  
Barnat, J., Brim, L., Češka, M., Ročkai, P., DiVinE: parallel distributed model checker (tool paper) (2010) Proceedings of Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology HiBi/PDMC 2010, pp. 4-7. , (Twente, The Netherlands), IEEE Computer Society Press, Sept
[3]  
Belinfante, A., Feenstra, J., de Vries, R.G., Tretmans, J., Goga, N., Feijs, L., Mauw, S., Heerink, L., Formal test automation: a simple experiment (1999) Proceedings of the IFIP 12th International Workshop on Testing of Communicating Systems IWTCS'99, , (Budapest, Hungary). Kluwer, Dordrecht, Sept
[4]  
Bergamini, D., Descoubes, N., Joubert, C., Mateescu, R., BISIMULATOR: a modular tool for on-the-fly equivalence checking (2005) Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2005, 3440, pp. 581-585. , (Edinburgh, Scotland, UK). Lecture Notes in Computer Science, Springer, Berlin, April
[5]  
Berthomieu, B., Bodeveix, J.-P., Farail, P., Filali, M., Garavel, H., Gaufillet, P., Lang, F., Vernadat, F., FIACRE: An intermediate language for model verification in the TOPCASED environment (2008) Proceedings of the 4th European Congress on Embedded Real-Time Software ERTS'08, , (Toulouse, France). SIA (the French Society of Automobile Engineers), AAAF (the French Society of Aeronautic and Aerospace), and SEE (the French Society for Electricity, Electronics, and Information & Communication T
[6]  
Blom, S., Orzan, S., Distributed state space minimization (2005) Softw. Tools Technol. Transfer, 7 (3), pp. 280-291
[7]  
Blom, S., van de Pol, J., Weber, M., LTSmin: distributed and symbolic reachability (2010) Proceedings of the 22nd International Conference on Computer Aided Verification CAV 2010, 6174, pp. 354-359. , (Edinburgh, UK). Lecture Notes in Computer Science. Springer, Berlin, July
[8]  
Bouajjani, A., Fernandez, J.-C., Graf, S., Rodríguez, C., Sifakis, J., Safety for branching time semantics (1991) Proceedings of 18th ICALP, , Springer, Berlin, July
[9]  
Bouali, A., Ressouche, A., Roy, V., de Simone, R., The Fc2Tools set: a toolset for the verification of concurrent systems (1996) Proceedings of the 8th Conference on Computer-Aided Verification, 1102. , (New Brunswick, New Jersey, USA). Lecture Notes in Computer Science. Springer, Berlin, Aug
[10]  
Boyer, F., Gruber, O., Salaün, G., Specifying and verifying the SYNERGY reconfiguration protocol with LOTOS NT/CADP (2011) Proceedings of the 17th International Symposium on Formal Methods FM'2011, 6664, pp. 103-117. , (Limerick, Ireland). Lecture Notes in Computer Science, Springer, Berlin, June
12345678910