Abstract
jMosel is a tool-set for the analysis and verification of linear parametric systems in monadic second-order logic on strings. In this paper we give a short introduction to the underlying concepts, as well as an overview of the implementation and the usage of jMosel.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Accellera Organization, Inc. Accellera Property Specification Language 1.1 Reference Manual (2004)
Basin, D.A., Klarlund, N.: Hardware Verification using Monadic Second- Order Logic. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 31–41. Springer, Heidelberg (1995)
Church, A.: Logic, arithmetic and automata. In: Proc. Intern. Congr. Math., pp. 23–35. Almqvist, Wiksells (1963)
Drechsler, R., Becker, B.: Binary Decision Diagrams: Theory and Implementation. Springer, Heidelberg (1998)
Jörges, S., Margaria, T., Steffen, B.: FormulaBuilder: A Tool for Graph-based Modelling and Generation of Formulae. In: ICSE 2006: Proceedings of the 28th international conference on Software engineering (2006)
Lind-Nielsen, J.: BuDDy (2006), http://sourceforge.net/projects/buddy
Margaria, T.: Fully Automatic Verification and Error Detection for Parameterized Iterative Sequential Circuits. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 258–277. Springer, Heidelberg (1996)
Margaria, T., Mendler, M.: Model-based Automatic Synthesis and Analysis in Second-OrderMonadic Logic. In: Proceedings AAS 1997, ACM/SIGPLAN Int. Worksh. on Automated Analysis of Software, pp. 99–112 (1997)
Margaria, T., Mendler, M., Gsottberger, C.: Modelling and Verification of Unbounded Length Systolic Arrays in Monadic Second Order Logic. In: Proc. Infinity 1998 - Int. Workshop on Infinite State Systems, satellite to ICALP 1998, SFB-Bericht 342/09/98A, pp. 9–23. TU Munich (1998)
Margaria, T., Nagel, R., Steffen, B.: Remote Integration and Coordination of Verification Tools in jETI. In: Proc. ECBS 2005, 12th IEEE Int. Conf. on the Engineering of Computer Based Systems, pp. 431–436. IEEE Computer Soc. Press, Los Alamitos (2005)
Møller, A.: Program Verification with Monadic Second-Order Logic & Languages for Web Service Development. Technical report, Brics, Daimi, PhD thesis (2002)
Nagel, R.: jABC (2006), http://jabc.cs.uni-dortmund.de
Nagel, R.: jETI, http://jeti.cs.uni-dortmund.de
Ranjan, R.: CAL BDD (2006), http://www-cad.eecs.berkeley.edu/Research/calbdd/
Somenzi, F.: CUDD (2006), http://vlsi.colorado.edu/fabio/CUDD/cuddIntrohtml
Vahidi, A.: JDD (2006), http://javaddlib.sourceforge.net/jdd/index.html
Whaley, J.: JavaBDD (2006), http://javabdd.sourceforge.net/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Topnik, C., Wilhelm, E., Margaria, T., Steffen, B. (2006). jMosel: A Stand-Alone Tool and jABC Plugin for M2L(Str). In: Valmari, A. (eds) Model Checking Software. SPIN 2006. Lecture Notes in Computer Science, vol 3925. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691617_18
Download citation
DOI: https://doi.org/10.1007/11691617_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33102-5
Online ISBN: 978-3-540-33103-2
eBook Packages: Computer ScienceComputer Science (R0)