
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Henrik Bohnenkamp, Pedro R. D'Argenio, Holger Hermanns, JoostPieter Katoen, "MODEST: A Compositional Modeling Formalism for Hard and Softly Timed Systems," IEEE Transactions on Software Engineering, vol. 32, no. 10, pp. 812830, October, 2006.  
BibTex  x  
@article{ 10.1109/TSE.2006.104, author = {Henrik Bohnenkamp and Pedro R. D'Argenio and Holger Hermanns and JoostPieter Katoen}, title = {MODEST: A Compositional Modeling Formalism for Hard and Softly Timed Systems}, journal ={IEEE Transactions on Software Engineering}, volume = {32}, number = {10}, issn = {00985589}, year = {2006}, pages = {812830}, doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2006.104}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  MODEST: A Compositional Modeling Formalism for Hard and Softly Timed Systems IS  10 SN  00985589 SP812 EP830 EPD  812830 A1  Henrik Bohnenkamp, A1  Pedro R. D'Argenio, A1  Holger Hermanns, A1  JoostPieter Katoen, PY  2006 KW  Modeling formalism KW  compositionality KW  formal semantics KW  timed automata KW  stochastic processes. VL  32 JA  IEEE Transactions on Software Engineering ER   
[1] M. Abadi and A.D. Gordon, “A Calculus for Cryptographic Protocols: The SPI Calculus,” Information and Computing, vol. 148, no. 1, pp. 170, 1999.
[2] L. Aceto, “A Static View of Localities,” Formal Aspects of Computing, vol. 6, pp. 201222, 1994.
[3] R. Alur et al., “The Algorithmic Analysis of Hybrid Systems,” Theoretical Computer Science, vol. 138, no. 1, pp. 334, 1995.
[4] R. Alur and D.L. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, no. 2, pp. 183235, 1994.
[5] C. Baier, F. Ciesinski, and M. Groesser, “Probmela: A Modeling Language for Communicating Probabilistic Processes,” Proc. Int'l Conf. Formal Methods and Models for Codesign (MEMOCODE '04), 2004.
[6] G. Behrmann, A. David, and K.G. Larsen, “A Tutorial on Uppaal,” Proc. Int'l Conf. Formal Modelling and Analysis of Timed Systems (FORMATS '04), 2004.
[7] M. BenAri, Principles of Concurrent and Distributed Programming. Prentice Hall, 1990.
[8] G. Berry, “Preemption and Concurrency,” Foundations of Software Technology and Theoretical Computer Science, pp. 7293, 1993.
[9] H. Bohnenkamp, J. Gorter, J. Guidi, and J.P. Katoen, “Are You Still There?—A Lightweight Algorithm to Monitor Node Presence in SelfConfiguring Networks,” Proc. Int'l Conf. Dependable Systems and Networks (DSN '05), pp. 704709, June 2005.
[10] H. Bohnenkamp, H. Hermanns, J.P. Katoen, and J. Klaren, “The Modest Modelling Tool and Its Implementation,” Proc. Conf. Computer Performance Evaluation: Modelling Techniques and Tools (TOOLS '03), pp. 116133, 2003.
[11] H. Bohnenkamp, H. Hermanns, J. Klaren, A. Mader, and Y.S. Usenko, “Synthesis and Stochastic Assessment of Schedules for Lacquer Production,” Proc. Int'l Conf. Quantitative Evaluation of Systems (QEST '04), 2004.
[12] T. Bolognesi and E. Brinksma, “Introduction to the Formal Description Technique LOTOS,” Computer Networks, vol. 14, pp.2559, 1987.
[13] S. Bornot and J. Sifakis, “An Algebraic Framework for Urgency,” Information and Computation, vol. 163, pp. 172202, 2001.
[14] M. Bravetti and P.R. D'Argenio, “Tutte le Algebre Insieme: Concepts, Discussions and Relations of Stochastic Process Algebras with General Distributions,” Validation of Stochastic Systems, LNCS 2925, pp. 4488, SpringerVerlag, 2004.
[15] M. Bravetti and R. Gorrieri, “The Theory of Interactive Generalised SemiMarkov Processes,” Theoretical Computer Science, vol. 286, no. 1, pp. 532, 2002.
[16] S. Cattani, R. Segala, M.Z. Kwiatkowska, and G. Norman, “Stochastic Transition Systems for Continuous State Spaces and NonDeterminism,” Proc. Conf. Foundations of Software Science and Computation Structures (FOSSACS '05), pp. 125139, 2005.
[17] D. Cavin, Y. Sasson, and A. Schiper, “On the Accuracy of MANET Simulators,” Principles of Mobile Computing, pp. 3843, ACM Press, 2002.
[18] G. Ciardo and R. Zijal, “WellDefined Stochastic Petri Nets,” Modeling, Analysis and Simulation of Computer and Telecommunication Systems, SCS Simulation Series, pp. 278284, 1996.
[19] D. Deavours, G. Clark, T. Courtney, D. Daly, S. Derasavi, J. Doyle, W.H. Sanders, and P. Webster, “The Mobius Framework and Its Implementation,” IEEE Trans. Software Eng. vol. 28, no. 10, pp. 956970, Oct. 2002.
[20] D.D. Deavours and W.H. Sanders, “An Efficient WellSpecified Check,” Proc. Int'l Workshop Petri Nets and Performance Models (PNPM '99), pp. 124133, 1999.
[21] P.R. D'Argenio, “Algebras and Automata for Timed and Stochastic Systems,” PhD thesis, Dept. of Computer Science, Univ. of Twente, 1999.
[22] P.R. D'Argenio and E. Brinksma, “A Calculus for Timed Automata,” Proc. Int'l Symp. Formal Techniques in RealTime and Fault Tolerant Systems (FTRTFT '96), pp. 110129, 1996.
[23] P.R. D'Argenio and B. Gebremichael, “The Coarsest Congruence for Timed Automata with Deadlines Contained in Bisimulation,” Proc. Int'l Conf. Concurrency Theory (CONCUR '05), pp. 125140, 2005.
[24] P.R. D'Argenio and B. Gebremichael, Axiomatising Timed Automata with Deadlines, technical report, 2006, to appear.
[25] P.R. D'Argenio, H. Hermanns, and J.P. Katoen, “On Generative Parallel Composition,” Electronic Notes on Theoretical Computer Science, vol. 22, 1999.
[26] P.R. D'Argenio, H. Hermanns, J.P. Katoen, and J. Klaren, “Modest: A Modelling Language for Stochastic Timed Systems,” Joint Int'l Workshop Process Algebra and Performance Modelling and Probabilistic Methods in Verification (PAPMPROBMIV '01), pp. 87104, 2001.
[27] P.R. D'Argenio, J.P. Katoen, and E. Brinksma, “An Algebraic Approach to the Specification of Stochastic Systems,” Programming Concepts and Methods, pp. 126147, Chapman & Hall, 1998.
[28] P.R. D'Argenio, J.P. Katoen, and E. Brinksma, “Specification and Analysis of Soft RealTime Systems: Quantity and Quality,” RealTime Systems Symp. (RTSS '99), pp. 104114, 1999.
[29] J. Desharnais, “Labeled Markov Process,” PhD thesis, McGill Univ., Montréal, 1999.
[30] S. Edwards, L. Lavagno, E.A. Lee, and A. SangiovanniVincentelli, “Design of Embedded Systems: Formal Models, Validation and Synthesis,” Proc. IEEE, vol. 85, no. 3, pp. 366390, 1997.
[31] E.A. Feinberg and A. Shwartz, Handbook of Markov Decision Processes. Kluwer, 2002.
[32] H. Garavel and M. Sighireanu, “A Graphical Parallel Composition Operator for Process Algebras,” Proc. Conf. Formal Techniques for Networked and Distributed Systems (FORTE '99), pp. 185202, 1999.
[33] H. Garavel and M. Sighireanu, “On the Introduction of Exceptions in ELOTOS,” Proc. Conf. Formal Techniques for Networked and Distributed Systems (FORTE '96), pp. 469484, 1996.
[34] P.W. Glynn, “A GSMP Formalism for Discrete Event Simulation,” Proc. IEEE, vol. 77, no. 1, pp. 1423, 1989.
[35] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic Model Checking for RealTime Systems,” Information and Computation, vol. 111, pp. 193244, 1994.
[36] H. Hermanns, U. Herzog, and J.P. Katoen, “Process Algebra for Performance Evaluation,” Theoretical Computer Science, vol. 274, pp. 4387, 2002.
[37] H. Hermanns and D. Turetayev, “A Generalisation of the WellSpecified Check,” Proc. Int'l Workshop Performability Modeling of Computer and Comm. (PMCCS), pp. 6266, 2003.
[38] J. Hillston, “A Compositional Approach to Performance Modelling,” PhD thesis, Univ. of Edinburgh, 1994.
[39] G.J. Holzmann, The Spin Model Checker. AddisonWesley, 2002.
[40] C. Hoare, Communicating Sequential Processes. Prentice Hall, 1985.
[41] ISO/IEC International Standard 15437, Information Technology— ELOTOS, Int'l Organization for Standardization, 2001.
[42] D.N. Jansen, H. Hermanns, and Y.S. Usenko, “From Stocharts to Modest: A Comparative Reliability Analysis of Train Radio Communications,” Proc. Workshop Software and Performance (WOSP'05), pp. 1323, 2005.
[43] J. Kramer and J. McGee, Concurrency: State Models and Java Programs. John Wiley and Sons, 1999.
[44] V.G. Kulkarni, Modeling and Analysis of Stochastic Systems. Chapman & Hall, 1995.
[45] M.Z. Kwiatkowska, G. Norman, R. Segala, and J. Sproston, “Automatic Verification of RealTime Systems with Discrete Probability Distributions,” Theoretical Computer Science, vol. 282, pp. 101150, 2002.
[46] E.A. Lee, “Embedded Software,” Advances in Computers, M.Zelkowitz, ed., vol. 56, Academic, 2002.
[47] D. Luckham and W. Polak, “ADA Exception Handling: An Axiomatic Approach,” ACM Trans. Programming Languages and Systems, vol. 2, no. 2, pp. 225233, 1980.
[48] N. Lynch and F.W. Vaandrager, “Action Transducers and Timed Automata,” Formal Aspects of Computing, vol. 8, no. 5, pp. 499538, 1996.
[49] A. Mader, H. Bohnenkamp, Y.S. Usenko, D.N. Jansen, J. Hurink, and H. Hermanns, “Synthesis and Stochastic Assessment of CostOptimal Schedules,” Technical Report 0614, Univ. Twente, 2006.
[50] V. Mertsiotakis, “Approximate Analysis Methods for Stochastic Process Algebras,” PhD thesis, Univ. of ErlangenNürnberg, 1998.
[51] R. Milner, Communication and Concurrency. Prentice Hall, 1989.
[52] R. Milner, Communicating and Mobile Systems: The $\pi\hbox{Calculus}$ . Cambridge Univ. Press, 1999.
[53] G.D. Plotkin, “A Structural Approach to Operational Semantics,” Report DAIMI FN19, Computer Science Dept., Aarhus Univ., 1981.
[54] J.C. Reynolds, Theories of Programming Languages. Cambridge Univ. Press, 1998.
[55] R. Segala and N.A. Lynch, “Probabilistic Simulations for Probabilistic Processes,” Nordic J. Comp., vol. 2, no. 2, pp. 250273, 1995.
[56] A.N. Shiryaev, “Probability,” Graduate Texts in Math., vol. 95, 1996.
[57] M. Sighireanu, “LOTOS NT User's Manual,” version 2.4, technical report, INRIA RhôneAlpes/VASY, 2004.
[58] A. Sokolova and E.P. de Vink, “Probabilistic Automata: System Types, Parallel Composition and Comparison,” Validation of Stochastic Systems, LNCS 2925, pp. 143, SpringerVerlag, 2004.
[59] W. Yi, P. Pettersson, and M. Daniels, “Automatic Verification of RealTime Communicating Systems by Constraint Solving,” Proc. Conf. Formal Techniques for Networked and Distributed Systems (FORTE '94), pp. 223238, 1994.
[60] W. Yi, “RealTime Behaviour of Asynchronous Agents,” Proc. Int'l Conf. Concurrency Theory (CONCUR '90), pp.502520, 1990.