Navegar

Colección

Datos Estadísticas

Artículo

Pavese, E.; Braberman, V.; Uchitel, S. "Probabilistic Interface Automata" (2016) IEEE Transactions on Software Engineering. 42(9):843-865
Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

System specifications have long been expressed through automata-based languages, which allow for compositional construction of complex models and enable automated verification techniques such as model checking. Automata-based verification has been extensively used in the analysis of systems, where they are able to provide yes/no answers to queries regarding their temporal properties. Probabilistic modelling and checking aim at enriching this binary, qualitative information with quantitative information, more suitable to approaches such as reliability engineering. Compositional construction of software specifications reduces the specification effort, allowing the engineer to focus on specifying individual component behaviour to then analyse the composite system behaviour. Compositional construction also reduces the validation effort, since the validity of the composite specification should be dependent on the validity of the components. These component models are smaller and thus easier to validate. Compositional construction poses additional challenges in a probabilistic setting. Numerical annotations of probabilistically independent events must be contrasted against estimations or measurements, taking care of not compounding this quantification with exogenous factors, in particular the behaviour of other system components. Thus, the validity of compositionally constructed system specifications requires that the validated probabilistic behaviour of each component continues to be preserved in the composite system. However, existing probabilistic automata-based formalisms do not support specification of non-deterministic and probabilistic component behaviour which, when observed through logics such as pCTL, is preserved in the composite system. In this paper we present a probabilistic extension to Interface Automata which preserves pCTL properties under probabilistic fairness by ensuring a probabilistic branching simulation between component and composite automata. The extension not only supports probabilistic behaviour but also allows for weaker prerequisites to interfacing composition, that supports delayed synchronisation that may be required because of internal component behaviour. These results are equally applicable as an extension to non-probabilistic Interface Automata. © 2016 IEEE.

Registro:

Documento: Artículo
Título:Probabilistic Interface Automata
Autor:Pavese, E.; Braberman, V.; Uchitel, S.
Filiación:Departamento de Computacion, Universidad de Buenos Aires, Argentina
Departamento de Computacion, Universidad de Buenos Aires, CONICET, Argentina
Departamento de Computacion, Universidad de Buenos Aires, Imperial College London, Argentina
Palabras clave:Behaviour models; interface automata; model checking; probability; Automata theory; Probability; Specifications; Behaviour models; Interface automata; Probabilistic extension; Probabilistic modelling; Qualitative information; Quantitative information; Reliability engineering; Software Specification; Model checking
Año:2016
Volumen:42
Número:9
Página de inicio:843
Página de fin:865
DOI: http://dx.doi.org/10.1109/TSE.2016.2527000
Título revista:IEEE Transactions on Software Engineering
Título revista abreviado:IEEE Trans Software Eng
ISSN:00985589
CODEN:IESED
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00985589_v42_n9_p843_Pavese

Referencias:

  • Clarke, E., Grumberg, O., Peled, D., (1999) Model Checking, , Cambridge MA USA: MIT Press
  • Musa, J., Operational profiles in software reliability engineering (1993) IEEE Softw., 10 (2), pp. 14-32. , Mar
  • Wu, S.-H., Smolka, S., Stark, E., Composition and behaviors of probabilistic I/O automata (1997) Theoretical Comput. Sci., 176 (1), pp. 1-38
  • Christoff, I., Testing equivalences and fully abstract models for probabilistic processes (1990) Proc. Theories Concurrency : Unification Extension, pp. 126-138
  • Van Glabbeek, R., Smolka, S., Steffen, B., Reactive, generative, and stratified models of probabilistic processes (1995) Inf. Comput., 121 (1), pp. 59-80
  • D'Argenio, P., Hermanns, H., Katoen, J.-P., On generative parallel composition (1999) Electron. Notes Theoretical Comput. Sci., 22, pp. 30-54
  • Sokolova, A., De Vink, E., Probabilistic automata: System types, parallel composition and comparison (2004) Validation of Stochastic Systems, pp. 1-43. , Berlin, Germany: Springer
  • Pavese, E., Braberman, V., Uchitel, S., Probabilistic environments in the quantitative analysis of (non-probabilistic) behaviour models (2009) Proc. 7th Joint Meeting Eur. Softw. Eng. Conf. ACM SIGSOFT Symp. Found. Softw. Eng, pp. 335-344
  • Henzinger, T., De Alfaro, L., Interface automata (2001) ACM SIGSOFT Softw. Eng. Notes, 26 (5), pp. 109-120
  • Segala, R., Lynch, N., Probabilistic simulations for probabilistic processes (1995) Nordic J. Comput., 2 (2), pp. 250-273
  • Hinton, A., Kwiatkowska, M., Norman, G., Parker, D., PRISM:A tool for automatic verification of probabilistic systems (2006) Proc. 6th Int. Conf. Tools Algorithms Construction Anal. Syst, pp. 441-444
  • Lynch, N., Tuttle, M., Hierarchical correctness proofs for distributed algorithms (1987) Proc. 6th ACM Symp. Principles Distrib. Comput, pp. 137-151
  • Halmos, P., (1976) Measure Theory (Graduate Texts in Mathematics Book), 18. , New York, New York, USA: Springer
  • Keller, R., Formal verification of parallel programs (1976) Commun., 19 (7), pp. 371-384
  • Baier, C., Groesser, M., Ciesinski, F., Quantitative analysis under fairness constraints (2009) Proc. 7th Int. Symp. Autom. Technol. Verif. Anal, pp. 135-150
  • Vardi, M., Automatic verification of probabilistic concurrent finite state programs (1985) Proc. 26th Annu. Symp. Found. Comput. Sci, pp. 327-338. , Oct
  • Baier, C., Kwiatkowska, M., Model checking for a probabilistic branching time logic with fairness (1998) Distrib. Comput., 11 (3), pp. 125-155. , Aug
  • Emerson, E.A., Clarke, E., Using branching time temporal logic to synthesize synchronization skeletons (1982) Sci. Comput. Programm., 2 (3), pp. 241-266. , Dec
  • De Nicola, R., Vaandrager, F., Action versus state based logics for transition systems (1990) Semantics Syst. Concurrent Processes, 469, pp. 407-419
  • Segala, R., (1995) Modeling and Verification of Randomized Distributed Real-time Systems, , Ph.D. dissertation Massachusetts Instit. Technol., Cambridge, MA, USA
  • De Alfaro, L., (1997) Formal Verification of Probabilistic Systems, , Ph.D. dissertation Stanford Univ., Stanford, CA, USA
  • Feller, W., (1968) An Introduction to Probability Theory and Its Applications, , New York NY USA: Wiley
  • Kulkarni, V., (2009) Modeling and Analysis of Stochastic Systems, , Boca Raton FL USA: CRC Press
  • Milner, R., (1989) Communication and Concurrency, , Englewood Cliffs, NJ USA: Prentice-Hall
  • Aziz, A., Singhal, V., Balarin, F., Brayton, R., Sangiovanni-Vincentelli, A., It usually works: The temporal logic of stochastic systems (1995) Proc. 26th Int. Conf. Comput. Aided Verif, pp. 155-165
  • Epifani, I., Ghezzi, C., Mirandola, R., Tamburrelli, G., Model evolution by run-time parameter adaptation (2009) Proc. Int. Conf. Softw. Eng, pp. 111-121
  • Cheung, R., A user-oriented software reliability model (1980) IEEE Trans. Softw. Eng., SE-6 (2), pp. 118-125. , Mar
  • Rodrigues, G.N., Rosenblum, D.S., Uchitel, S., Sensitivity analysis for a scenario-based reliability prediction model (2005) SIGSOFT Softw. Eng. Notes, 30 (4), pp. 1-5. , May
  • Go-Seva-Popstojanova, K., Trivedi, K.S., Architecture-based approach to reliability assessment of software systems (2001) Perform. Eval., 45 (2-3), pp. 179-204
  • Yacoub, S., Cukic, B., Ammar, H., A scenario-based reliability analysis approach for component-based software (2004) IEEE Trans. Rel., 53 (4), pp. 465-480. , Dec
  • Roshandel, R., Medvidovic, N., Toward architecture-based reliability estimation (2004) Proc. ICSE Workshop Architecting Dependable Syst, pp. 2-6
  • Hoare, C.A.R., Communicating sequential processes (1978) Commun ACM, 21 (8), pp. 666-677
  • Hierons, R.M., Nunez, M., Testing probabilistic distributed systems (2010) Proc. Formal Techn. Distrib. Syst., pp. 63-77
  • Delahaye, B., Caillaud, B., Legay, A., Probabilistic contracts: A compositional reasoning methodology for the design of systems with stochastic and/or non-deterministic aspects (2011) Formal Methods Syst. Des., 38, pp. 1-32
  • Kwiatkowska, M., Norman, G., Parker, D., Qu, H., Assumeguarantee verification for probabilistic systems (2010) Proc. 16th Int. Conf. Tools Algorithms Construction Anal. Syst., pp. 23-37
  • Hermanns, H., Krcal, J., Kretnsky, J., Compositional verification and optimization of interactive Markov chains (2013) Proc. CONCUR-Concurrency Theory, pp. 364-379
  • Hermanns, H., Katoen, J.-P., The how and why of interactive Markov chains (2009) Proc. 8th Int. Symp. Formal Methods for Components Objects, pp. 311-337
  • Hansson, H., Jonsson, B., A calculus for communicating systems with time and probabilities (1990) Proc. 11th Real-Time Syst. Symp, pp. 278-287
  • Smolka, S., Jou, C.-C., Equivalences, congruences, and complete axiomatizations for probabilistic processes (1990) Proc. CONCUR Theories Concurrency: Unification Extension, pp. 367-383
  • Baier, C., Hermanns, H., Weak bisimulation for fully probabilistic processes (1997) Proc. 9th Int. Conf. Comput. Aided Verification, pp. 119-130
  • Philippou, A., Lee, I., Sokolsky, O., Weak bisimulation for probabilistic systems (2000) Proc. 11th Int. Conf. Concurrency Theory, 1877, pp. 334-349
  • Cattani, S., Segala, R., Decision algorithms for probabilistic bisimulation (2002) Proc. 13th Int. Conf. Concurrency Theory, pp. 371-386

Citas:

---------- APA ----------
Pavese, E., Braberman, V. & Uchitel, S. (2016) . Probabilistic Interface Automata. IEEE Transactions on Software Engineering, 42(9), 843-865.
http://dx.doi.org/10.1109/TSE.2016.2527000
---------- CHICAGO ----------
Pavese, E., Braberman, V., Uchitel, S. "Probabilistic Interface Automata" . IEEE Transactions on Software Engineering 42, no. 9 (2016) : 843-865.
http://dx.doi.org/10.1109/TSE.2016.2527000
---------- MLA ----------
Pavese, E., Braberman, V., Uchitel, S. "Probabilistic Interface Automata" . IEEE Transactions on Software Engineering, vol. 42, no. 9, 2016, pp. 843-865.
http://dx.doi.org/10.1109/TSE.2016.2527000
---------- VANCOUVER ----------
Pavese, E., Braberman, V., Uchitel, S. Probabilistic Interface Automata. IEEE Trans Software Eng. 2016;42(9):843-865.
http://dx.doi.org/10.1109/TSE.2016.2527000