Composing, analyzing and validating software models to assess the performability of competing design candidates

Annals of Software Engineering - Tập 8 - Trang 239-287 - 1999
Frederick T. Sheldon1, Stefan Greiner2
1School of Electrical Engineering and Computer Science, Washington State University, Pullman, USA
2Performance Modeling & Process Control Research Group, Department of Computer Science IMMD IV, The University of Erlangen‐Nürnberg, Erlangen, Germany E-mail: [email protected]

Tóm tắt

In a perfect world, verification and validation of a software design specification would be possible before any code was generated. Indeed, in a perfect world we would know that the implementation was correct because we could trust the class libraries, the development tools, verification tools and simulations, etc. These features would provide the confidence needed to know that all aspects (complexity, logical and timing correctness) of the design were fully satisfied (i.e., everything was right). Right in the sense that we built it right (it is correct with respect to its specification) and it solves the right problem. Unfortunately, it is not a perfect world, and therefore we must strive to continue to refine, develop and validate useful methods and tools for the creation of safe and correct software. This paper considers the analysis of systems expressed using formal notations. We introduce our framework, the modeling cycle, and motivate the need for tool supported rigorous methods. Our framework is about using systematic formal techniques for the creation and composition of software models that can further enable reasoning about high‐assurance systems. We describe several formal modeling techniques within this context (i.e., reliability and availability models, performance and functional models, performability models, etc.). This discussion includes a more precise discourse on stochastic methods (i.e., DTMC and CTMC) and their formulation. In addition, we briefly review the underlying theories and assumptions that are used to solve these models for the measure of interest (i.e., simulation, numerical and analytical techniques). Finally, we present a simple example that employs generalized stochastic Petri nets and illustrates the usefulness of such analysis methods.

Từ khóa


Tài liệu tham khảo

Allen, O. (1978), Probability, Statistics and Queuing Theory, Academic Press, New York, NY.

Allen, O. (1990), Probability, Statistics and Queuing Theory, 2nd Edition, Academic Press, New York, NY.

Allmaier, S.C., M. Kowarschik, and G. Horton (1997), “State Space Construction and Steady-State Solution of GSPNs on a Shared-Memory Multiprocessor,” In 7th Int. Workshop on Petri Nets and Performance Models, IEEE Computer Society Press, Los Alamitos, CA, pp. 112–121.

Balbo, G. (1993), “Performance Evaluation and Concurrent Programming,” In Messung, Modellierung und Bewertung von Rechen-und Kommunikationssystemen, Springer-Verlag, Berlin, pp. 1–13.

Balbo, G. (1995), “On the Success of Stochastic Petri Nets,” In Int. Workshop on Petri Nets and Performance Modeling, IEEE CS Press, Los Alamitos, CA, pp. 2–9.

Balbo, G., S. Donatelli, and G. Franceschinis (1992), “Understanding Parallel Program Behavior through Petri Net Models,” Journal of Parallel and Distributed Computing 15,3, 171–187.

Balbo, G., S. Donatelli, G. Granceschinis, A. Mazzeo, N. Mazzocca, and M. Ribaudo (1994), “On the Computation of Performance Characteristics of Concurrent Programs Using GSPNs,” Performance Evaluation 19,18, 195–222.

Earner, J. (1994), “Entwicklung, Implementierung und Validierung von Analytischen Verfahren zur Anlyse von Prioritatsnetzen,” Masters thesis, Computer Science Department IMMD IV, University of Erlangen-Nürnberg, Germany.

Blake, J.T., A.L. Reibman, and K.S. Trivedi (1988), “Sensitivity Analysis of Reliability and Performability Measures for Multiprocessor Systems,” In SIGMETRICS, ACM, New York, NY, pp. 177–186.

Bolch, G. (1989), “Leitungsbewertung von Rechensystemen,” TR-1989-IMMD IV, Leitfaden und Monographien der Informatik-B.G. Teubner Verlagsgesellschaft, Stuttgart.

Buchholz, P. (1994), “Compositional Analysis of a Markovian Process Algebra,” In Proceedings PAPM, CLUP, pp. 233–245.

Burch, J.R., E.M. Clarke, and K.L. McMillan (1992), “Symbolic Modeling Checking: 1020 States and Beyond,” Information and Computation 98,42, 142–170.

Buzen, J. (1971), “Queuing Network Models of Multiprogramming,” Dissertation (Ph.D.), Division of Engineering and Applied Physics, Harvard, Cambridge, MA.

Calzarossa, M., and M. Massari (1991), “Workload Analyzer Tool — WAT — User Guide,” In Fifth Int. Conf. on Modeling Techniques and Tools for Computer Performance Evaluation, Univ. di Milano, Diparimento di Scienza dell'Informazione, pp. 1–15.

Carson, J. (1992), “Modeling,” Winter Simulation Conference (Group on Simulation), SIGSIM, ACM, New York, NY, pp. 82–87.

Chiola, G. (1985), “A Software Package for the Analysis of Generalized Stochastic Petri Net Models,” In Int. Workshop on Timed Petri Nets, IEEE Computer Society Press, Los Alamitos, CA, pp. 136–143.

Choi, H., V. Mainkar, and K.S. Trivedi (1993), “Sensitivity Analysis of Deterministic and Stochastic Petri Nets,” In MASCOTS'93 International Workshop on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, pp. 271–276.

Ciardo, G. (1987), “Toward a Definition of Modeling Power for Stochastic Petri Net Models,” In Int. Workshop on Petri Nets and Performance Models, IEEE Computer Society Press, Los Alamitos, CA, pp. 54–62.

Ciardo, G. and K.S. Trivedi (1993), “A decomposition approach for stochastic reward net models,” Performance Evaluation 18,1, 37–59.

Ciardo, G., R. Pricks, J. Muppala, and K.S. Trivedi (1994), “SPNP Users Manual Version 4.0,” TR-1993–10, Duke University, Department of EE, Durham, NC.

Ciardo, G., J. Muppala, and K.S. Trivedi (1989), “SPNP: Stochastic Petri Net Package,” In 3rd Int. Workshop on Petri Nets and Performance Models, IEEE Computer Society Press, Los Alamitos, CA, pp. 144–151.

Ciardo, G., J. Muppala, and K.S. Trivedi (1991), “On the Solution of GSPN Reward Models,” Performance Evaluation 12, 237–253.

Ciardo, G., J. Muppala, and K.S. Trivedi (1992a), “Analyzing Concurrent and Fault-Tolerant Software Using Stochastic Reward Nets,” Journal of Parallel and Distributed Computations 255–269.

Ciardo, G., R. Marie, S. Bruell, and K. Trivedi (1992b), “Performability Analysis Using Semi-Markov Reward Processes,” IEEE Transactions on Computers 39,10, 121–1264.

Ciardo, G., A. Blakemore, P.F. Chimento, J.K. Muppala, and K.S. Trivedi (1993), “Automated Generation and Analysis of Markov Reward Models Using Stochastic Rewards Nets,” In IMA Volumes in Mathematics and its Applications, C. Meyer and R.J. Plemmons, Eds, Springer-Verlag, Berlin, Germany, pp. 145–191.

Dedie, G. (1988), “Nucleus BS2000 — Technical Description,” TR-BS200–88.

Deitel, H.M. (1990), An Introduction to Operating Systems, Addison-Wesley, Reading, MA.

Donatelli, S., G. Franceschinis, N. Mazzocca, and S. Russo (1994), “Software Architecture of the EPOCA Integrated Environment,” In 7th Int. Conference on Performance Evaluation, Modeling Techniques and Tools, Lecture Notes in Computer Science, Vol. 794, Springer-Verlag, Berlin, pp. 335–352.

Donatelli, S., M. Ribaudo, and J. Hillston (1995), “A Comparison of Performance Evaluation Process Algebra and Generalized Stochastic Petri Nets,” In 5th Int. Workshop PNPM, IEEE Computer Society Press, Los Alamitos, CA, pp. 158–168.

Evan, J. (1988), Structures of Discrete Event Simulation: An Introduction to the Engagement Strategy, Ellis Horwood Limited, Chicester (W. Sussex), UK.

Fleischmann, G. (1989), “Modellierung und Bewertung Paralleler Programme,” Ph.D. dissertation, Computer Science IMMD IV, University of Erlangen-Nurnberg, Erlangen, Germany.

Gangl, P. (1993), “Simulation — eine Schlusseltechnologie der 90er Jahre: Hoher Nutzen aber geringer Kentnisstand in der Wirtschaft,” In 8th Symp. on Simulation Techniques, Vieweg-Verlag, Germany, pp. 103–106.

Gordon, W. and G. Newell (1967), “Closed Queuing Systems with Exponential Servers,” Operations Research 15,2, 245–265.

Greiner, S. (1993), “Leistungsbewertung des Betriebssystems UNIX mil Hilfe approximativer analytischer Methoden,” TR-1993–9, University of Erlangen, Computer Science Department IMMD IV, Erlangen, Germany.

Greiner, S. (1995a), “Performance Evaluation of Dynamic Priority Operating Systems,” In 5th Int. Workshop PNPM, IEEE Computer Society Press, Los Alamitos, CA, pp. ?.

Greiner, S. (1995b), “An Analytical Model for the Operating System BS2000,” Computer Science Department IMMD IV, University of Erlangen, Erlangen, Germany.

Greiner, S. (1999), “Stochastic Analysis of Computer Science Applications: Theory, Models and Solution Methods,” Ph.D. dissertation, Computer Science Department IMMD IV, University of Erlangen-Nurnberg, Germany.

Greiner, S. and G. Horton (1996), “Analysis of Stiff Markov Chains with the Multi-level Method,” In European Simulation Symposium, pp. 801–805.

Heidelberger, P. and A. Goyal (1988), “Sensitivity Analysis of Continuous Time Markov Chains Using Uniformization,” In Computer Performance and Reliability, Proc. of the 2nd Int. MCPR Workshop, North-Holland, Amsterdam, pp. 93–104.

Hein, A. and K.K. Goswami (1996), “Conjoint Simulation — A Technique for the Combined Performance and Dependability Analysis of Large-Scale Computer Systems,” In Advances in Simulation, IEEE Computer Society Press, Los Alamitos, CA, pp. 68–77.

Hoare, C.A.R. (1985), Communicating Sequential Processes, Prentice-Hall, London.

Holzmann, G.J. (1993), “Design and Validation of Protocols: A Tutorial,” Computer Networks and ISDN Systems 25, 981–1017.

Holzmann, G.J. (1997), “The Model Checker SPIN,” IEEE Transactions on Software Engineering 23,5, 279–295.

Horton, J. and S. Leutenegger (1994), “A Multi-Level Algorithm for Steady State Markov Chains,” In SIGMETRICS, ACM, New York, NY, pp. 191–200.

Horton, G. and S. Leutenegger (1995), “On the Utility of the Multi-Level Algorithm for the Solution of Nearly Completely Decomposable Markov Chains,” In Second Int. Workshop on the Numerical Solution of Markov Chains, Kluwer, Boston, pp. 425–442.

Jackson, J. (1963), “Jobshop-Like Queuing Systems,” Management Science 10,1, 131–142.

Kavi, K.M. and F.T. Sheldon (1994), “Specification of Stochastic Properties with CSP,” In Int. Conference on Parallel and Distributed Systems, IEEE Computer Society Press, Los Alamitos, CA, pp. 288–293.

Kleinrock, L. (1975), Queuing Systems, Vol. 1: Theory, Wiley, New York, NY.

Koller, D., D. McAllester, and A. Pfeffer (1997), “Effective Bayesian Inference for Stochastic Programs,” In Fourteenth Nat. Conf. AAAI, AAAI, Menlo Park, CA, pp. 740–747.

Laprie, J.C., M. Kaaniche, and K. Kanoun (1995), “Modeling Computer Systems Evolutions: Non-Stationary Processes and Stochastic Petri Nets — Application to Dependability Growth,” In Int. Workshop on Petri Nets and Performance Models, IEEE Computer Society Press, Los Alamitos, CA, pp. 221–230.

Lazowska, E.D., J. Zahorjan, G.S. Graham, and K.C. Sevcik (1984), Quantitative System Performance — Computer System Analysis Using Queuing Network Models, Prentice-Hall, London.

Levenson, N.G. and J.L. Stolzy (1987), “Safety Analysis Using Petri Nets,” IEEE Transactions on Software Engineering 13,3, 386–397.

Lewis, A.D. (1988), “Petri Net Modeling and Software Safety Analysis: Methodology for an Embedded Military Application,” Masters thesis, Computer Science, Naval Postgraduate School, Monterey, CA.

Liebl, F. (1995), Simulation, Oldenbourg, Munich.

Logothetis, D. and K.S. Trivedi (1997), “The Effect of Detection and Restoration Times for an Error Recovery in Communication Networks,” Journal of Network and Systems Management 5,2, 173–195.

Mainkar, V., H. Choi, and K. Trivedi (1993), “Sensitivity Analysis of Markov Regenerative Stochastic Petri Nets,” In 5th Int. Workshop on Petri Nets and Performance Modeling, IEEE Computer Society Press, Los Alamitos, CA, pp. 180–189.

Malhotra, M. and K.S. Trivedi (1993), “A Methodology for Formal Expression of Hierarchy in Model Solution,” In Fifth Int. Workshop on PNPM, IEEE Computer Society Press, Los Alamitos, CA, pp. 258–267.

Marie, R. and A. Jean-Marie (1993), “Quantitative Evaluation of Discrete-Event Systems: Models, Performance and Techniques,” In Fifth Int. Workshop on Petri-Nets and Performance Modeling, IEEE Computer Society Press, Los Alamitos, CA, pp. 2–11.

Marsan, M.A., G. Balbo, and G. Conte (1984), “A Class of Generalized Stochastic Petri Nets for the Performance Evaluation of Multiprocessor Systems,” ACM Transactions on Computer Systems 2,1, 93–122.

Milner, R. (1989), Communication and Concurrency, Prentice-Hall, London.

Molloy, M.K. (1982), “Performance Analysis Using Stochastic Petri Nets,” IEEE Transactions on Computers 31,9, 913–917.

Muppala, J.K., G. Ciardo, and K.S. Trivedi (1994a), “Stochastic Reward Nets for Reliability Prediction,” TR-1994–12, Duke University, EE Department, Durham, NC.

Muppala, J.K., W. Wang, and K.S. Trivedi (1994b), “Dependability Evaluation Through Measurements and Models,” Fnl. Rpt. NSF Grant CCR-9108114, Duke University, EE Department, Durham, NC.

Murata, T. (1989), “Petri Nets: Properties, Analysis and Applications,” Proceedings of the IEEE 77,4, 541–580.

Olderog, E.-R. (1986), “TCSP — Theory of communicating sequential processes,” In Lecture Notes in Computer Science Vol. 255, pp. 441–465.

Olderog, E.-R. (1987), “Operational Petri Net Semantics for CCSP,” In Lecture Notes in Computer Science Vol. 266, pp. 196–223.

Reibman, A., R. Smith, and K. Trivedi (1989), “Markov and Markov Reward Model Transient Analysis: An Overview of Numerical Approaches,” European Journal of Operational Research 40,2, 257–267.

Reibman, A. and M. Veeraraghavan (1991), “Reliability Modeling: A Modeling Overview for System designers,” Computer 24,4, 49–57.

Rettelbach, M. (1996), “Stochastic Process Algebras with Timeless Activities and Probabilistic Branching Probabilities,” Dissertation (Ph.D.), Computer Science Department, Friedrich Alexander Universitaet Erlangen-Nürnberg, Erlangen, Germany.

Sahner, R., K.S. Trivedi and A. Puliafito (1996), Performance and Reliability Analysis of Computer Systems — An Example-Based Approach Using the SHARPS Software Package, Kluwer Academic, Boston, MA.

Sahner, R. and K.S. Trivedi (1986), “Reliability Modeling Using SHARPE,” TR-1986–19, Computer Science, Duke University, Durham, NC.

Sahner, R.A. and K.S. Trivedi (1993), “A Software Tool for Learning About Stochastic Models,” IEEE Transactions on Education 36,1, 56–61.

Sanders, W., W. Obal, A. Qureshi, and F. Widjanarko (1995), “The UltraSAN Modeling Environment,” Performance Evaluation 24,1, 89–115.

Sanders, W.H. and J.F. Meyer (1991), “Reduced Base Model Construction Methods for Stochastic Activity Networks,” IEEE Journal on Selected Areas in Communications 9,1, 25–36.

Schweitzer, P. (1991), “A Survey of Aggregation-Disaggregation in Large Markov Chains,” In Numerical Solution of Markov Chains, W. Stewart, Ed., Marcel Dekker, New York, NY, pp. 150–230.

Sheldon, F.T. (1996), “Specification and Analysis of Stochastic Properties for Concurrent Systems Expressed Using CSP,” Ph.D. dissertation, UMI and CSE Department, University of TX at Arlington, Ann Arbor, MI.

Sheldon, F.T. (1998), “Analysis of Real-Time Concurrent System Models Based on CSP Using Stochastic Petri Nets,” In 12th European Simulation Multi-Conference, SCS Int., Amsterdam, pp. 776–783.

Sheldon, F.T. and K.M. Kavi (1995), “Linking Software Failure Behavior to Specification Characteristics II,” In 4th Int. Workshop on Evaluation Techniques for Dependable Systems, IEEE Computer Society Press, Los Alamitos, CA.

Sheldon, F.T., K.M. Kavi, and F.A. Kamangar (1995), “Reliability Analysis of CSP Specifications: A New Method Using Petri Nets,” Computing in Aerospace 10, AIAA, Reston, VA, pp. 317–326.

Siegle, M. (1995), “Bescgreibung und Analyse von Makovmodellen mil Grossem Zustandsraum,” Ph.D. dissertation, Computer Science Department IMMD IV, University Erlangen-Nürnberg, Germany.

Sommerville, I. (1996), Software Engineering, Fifth Edition, Addison-Wesley, Reading, MA.

Stewart, W.J. (1994), Introduction to the Numerical Solution of Markov Chains, Princeton University Press, Princeton, NJ.

Stiegler, H. (1988), “System Overview BS2000 — Technical Description,” 15–1988, Siemens Corp., Munich, Germany.

Trivedi, K.S. (1982), Probability and Statistics with Reliability, Queuing and Computer Science Applications, Prentice-Hall, Englewood Cliffs, NJ.

Trivedi, K. and M. Malhotra (1993), “Reliability and Performability Techniques and Tools: A Survey,” Messung, Modellierung und Bewertung von Rechen-und Kommunikationssystemen, Springer-Verlag, Berlin, pp. 27–48.

Villemeur, A. (1992), Reliability, Availability, Maintainability and Safety Assessment, Wiley, New York, NY.

Yen, I.-L., R. Paul, and K. Mori (1998), “Toward Integrated Methods for High-Assurance Systems,” IEEE Computer 31,4, 32–34 (including pp. 35–46 by others).