Istituto di Scienza e Tecnologie dell'Informazione     
Latella D., Loreti M., Massink M. On-the-fly fluid model checking via discrete time population models. In: EPEW 2015 - 12th European Workshop on Computer Performance Engineering (Madrid, Spain, 31 August - 1 September 2015). Proceedings, pp. 193 - 207. Marta Beltrán, William Knottenbelt, Jeremy Bradley (eds.). (Lecture Notes in Computer Science, vol. 9272). Springer, 2015.
We show that, under suitable convergence and scaling conditions, fluid model checking bounded CSL formulas on selected individuals in a continuous large population model can be approximated by checking equivalent bounded PCTL formulas on corresponding objects in a discrete time, time synchronous Markov population model, using an on-the-fly mean field approach. The proposed technique is applied to a benchmark epidemic model and a client-server case study showing promising results also for the challenging case of nested formulas with time dependent truth values. The on-the-fly results are compared to those obtained via global fluid model checking and statistical model-checking.
URL: http://link.springer.com/chapter/10.1007/978-3-319-23267-6_13
DOI: 10.1007/978-3-319-23267-6_13
Subject Fluid model-checking
Probabilistic model-checking
On-the-fly model-checking
Continuous Time Markov Chains
Discrete Time Markov Chains
B.8.2 Performance Analysis and Design Aids
D.2.4 Software/Program Verification
F.1.2 Modes of Computation
F.1.1 Models of Computation
F.3.1 Specifying and Verifying and Reasoning about Programs
39-XX Difference and functional equations
60Jxx Markov processes

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional