Abstract
Modest is a high-level compositional modelling language for stochastic timed systems with a formal semantics in terms of stochastic timed automata, an overarching formalism of which several well-studied models are special cases. The emphasis of Modest is to make use of existing analysis techniques and tools in a single-formalism, multiple-solution approach. In this paper, we focus on networks of timed automata as supported by Uppaal. We report on extensions made to Modest and Uppaal that allow the transformation of a rich subset of Modest models to Uppaal timed automata and enable connections to further tools and formalisms. We present our Modest-to-Uppaal tool chain mctau, which allows both a fully automated analysis as well as model transformation, and we compare its performance with the existing mcpta tool.
This work has been supported by the European Union FP7-ICT projects Quasimodo, contract no. 214755, and MEALS, contract no. 295261, by the DFG as part of SFB/TR 14 AVACS, and by the DFG/NWO Bilateral Research Program ROCKS.
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
Alur, R., Dill, D.L.: A theory of timed automata. TCS 126(2), 183–235 (1994)
Baró Graf, H., Hermanns, H., Kulshrestha, J., Peter, J., Vahldiek, A., Vasudevan, A.: A verified wireless safety critical hard real-time design. In: WoWMoM. IEEE (2011)
Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
Berrang, P., Bogdoll, J., Hahn, E.M., Hartmanns, A., Hermanns, H.: Dependability results for power grids with decentralized stabilization strategies. Reports of SFB/TR 14 AVACS 83 (2012) ISSN: 1860-9821, www.avacs.org
Bogdoll, J., Ferrer Fioriti, L.M., Hartmanns, A., Hermanns, H.: Partial Order Methods for Statistical Model Checking and Simulation. In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol. 6722, pp. 59–74. Springer, Heidelberg (2011)
Bohnenkamp, H.C., D’Argenio, P.R., Hermanns, H., Katoen, J.-P.: MoDeST: A compositional modeling formalism for hard and softly timed systems. IEEE Transactions on Software Engineering 32(10), 812–830 (2006)
Bohnenkamp, H.C., Hermanns, H., Katoen, J.-P.: motor:The modest Tool Environment. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 500–504. Springer, Heidelberg (2007)
Bornot, S., Sifakis, J.: An algebraic framework for urgency. Inf. Comput. 163(1), 172–202 (2000)
D’Argenio, P.R., Katoen, J.-P., Ruys, T.C., Tretmans, J.: The Bounded Retransmission Protocol Must be on Time! In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 416–431. Springer, Heidelberg (1997)
Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372–387. Springer, Heidelberg (2011)
Haas, P.J., Shedler, G.S.: Regenerative generalized semi-Markov processes. Communications in Statistics. Stochastic Models 3(3), 409–438 (1987)
Hartmanns, A.: Model-Checking and Simulation for Stochastic Timed Systems. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO. LNCS, vol. 6957, pp. 372–391. Springer, Heidelberg (2011)
Hartmanns, A., Hermanns, H.: A Modest approach to checking probabilistic timed automata. In: QEST, pp. 187–196. IEEE Computer Society (2009)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)
Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. TCS 282(1), 101–150 (2002)
Mader, A., Bohnenkamp, H.C., Usenko, Y.S., Jansen, D.N., Hurink, J., Hermanns, H.: Synthesis and stochastic assessment of cost-optimal schedules. STTT 12(5), 305–318 (2010)
Norman, G., Palamidessi, C., Parker, D., Wu, P.: Model checking the probabilistic pi-calculus. In: QEST, pp. 169–178. IEEE Computer Society (2007)
Yue, H., Bohnenkamp, H., Kampschulte, M., Katoen, J.-P.: Analysing and Improving Energy Efficiency of Distributed Slotted Aloha. In: Balandin, S., Koucheryavy, Y., Hu, H. (eds.) NEW2AN 2011 and ruSMART 2011. LNCS, vol. 6869, pp. 197–208. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bogdoll, J., David, A., Hartmanns, A., Hermanns, H. (2012). mctau: Bridging the Gap between Modest and UPPAAL. In: Donaldson, A., Parker, D. (eds) Model Checking Software. SPIN 2012. Lecture Notes in Computer Science, vol 7385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31759-0_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-31759-0_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31758-3
Online ISBN: 978-3-642-31759-0
eBook Packages: Computer ScienceComputer Science (R0)