Formal specification of the Mobius modeling framework

Modern computer and communication systems are becoming increasingly complex, and predicting the performance, dependability, and performability of such systems is challenging. A number of modeling formalisms have been developed to model certain types of systems, or aspects of a complex system, but no single formalism has proven to be ideal for all systems. Furthermore, no single way of solving models has been shown to be universally applicable and effective.; We have developed Möbius to address these challenges. Möbius is a complete, coherent, and consistent framework for building a software tool for the performance and dependability evaluation of complex, discrete-event systems. Möbius allows modelers to create models using a variety of formalisms supported by the framework. Models, possibly expressed in different formalisms, can then be composed together to form larger models. This allows users to use the formalism best suited for modeling a portion of the overall model. Furthermore, formalisms used to compose models together can operate on models without knowledge of the formalism that was used to create the submodels. Finally, solvers interact with Möbius models, as opposed to formalism models. Careful use of “properties” allows the application of efficient solvers to models.; A number of features make Möbius unique. First, we are unaware of any other approach that allows models to be created using very different formalisms and then to be composed structurally to form a single new model using composition formalisms. While the Möbius framework defines a universe of possible models, we avoid trying to create a “universal formalism” and instead try to create a general framework that supports a large variety of modeling formalisms.; In this thesis, we describe the Möbius framework and illustrate its usefulness by showing mappings from many formalisms into the framework. We also address some fundamental issues in the field of modeling of discrete-event systems, namely an efficient well-specified checker and a general, structured execution policy. Finally, we have developed a formalism to illustrate many of the features developed for Möbius but not found in any previously existing formalisms.