- 9:00am—10:00am, Keynote
Multi‐Agent Networked Systems with Adversarial Elements.
- 10:00am—11:00am, Kronecker and product form methods
. A matrix-free structured solution for Markov Regenerative Processes.
. Low-rank tensor methods for communicating Markov processes.
- 11:30am—1:00pm, Hybrid systems
. A statistical approach for computing reachability of non-linear and stochastic dynamical systems.
. Formal Synthesis and Validation of Inhomogeneous Thermostatically Controlled Loads.
. Finite Abstractions of Stochastic Max-Plus-Linear Systems.
- 2:30pm—4:00pm, Mean-field/population analysis
. Mean field for performance models with generally distributed-timed transitions.
. Mean-Field approximation and Quasi-Equilibrium reduction of Markov Population Models.
. On performance of Gossip communication in a crowd-sensing scenario.
- 4:30pm—6:00pm, Models and tools
. Probabilistic Model Checking of DTMC Models of User Activity Patterns.
. Performance Comparison of IEEE 802.11 DCF and EDCA for Beaconing in Vehicular Networks.
. A new GreatSPN GUI for GSPN editing and CSLTA model checking (tool paper).
. The Octave queueing Package (tool paper).
- 6:30pm—11:00pm, Reception at Villa Bardini
- 9:00am—10:00am, Keynote (joint program with FORMATS)
(University of North Carolina at Chapel Hill). The Modeling and Analysis of Mixed-Criticality Systems.
- 10:00am—11:00am, Simulation
. A perfect sampling algorithm of random walks with forbidden arcs.
. Modelling Replication in NoSQL Datastores.
- 11:30am—1:00pm, Queueing, debugging, and tools
. On queues with general service demands and constant service capacity.
. Simulation Debugging and Visualization in the Mobius Modeling Framework.
. Scalar: A distributed benchmarking framework for systematic scalability analysis (tool paper).
. Non-Intrusive Scalable Memory Access Tracer (tool paper).
- 2:30pm—4:00pm, Process algebras and equivalencies
. Probabilistic Programming Process Algebra.
. PALOMA: A Process Algebra for Located Markovian Agents.
. On the Discriminating Power of Testing Equivalences for Reactive Probabilistic Systems: Results and Open Problems.
- 4:30pm—6:00pm, Automata and Markov process theory
. Continuity Properties of Distances for Markov Processes.
. Deciding the value 1 problem for reachability in 1-clock decision stochastic timed automata.
. Decidable Problems for Unary PFAs.
- 8:00pm—11:30pm, Social dinner at Castello dell'Acciaiolo
- 9:00am—10:00am, Keynote (joint program with SAFECOMP)
(University of Coimbra). Quantitative safety assessment: experiments and field measurements.
- 10:00am—11:00am, Fault Injection Techniques (SAFECOMP Session)
. A Simulated Fault Injection Framework for Time-Triggered Safety-Critical Embedded Systems.
. Rapid Fault-Space Exploration by Evolutionary Pruning.
- 11:30am—1:00pm, Applications, theory, and tools
. A Scalable Approach to the Assessment of Storm Impact in Distributed Automation Power Grids.
. Compositionality Results for Quantitative Information Flow.
. CyberSAGE: A Tool for Automatic Security Assessment of Cyber-Physical Systems (tool paper).
Tool demonstrations (also during lunch).
- 2:30pm—3:30pm, Keynote
(Universität Würzburg). Quantitative Evaluation of Service Dependability in Shared Execution Environments.
- 3:30pm—4:30pm, Probabilistic Model Checking
. Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains.
. Accelerating Parametric Probabilistic Verification.
- 5:00pm—6:00pm, Verification & Validation Techniques (SAFECOMP Session)
. Safety Validation of Sense and Avoid Algorithms using Simulation and Evolutionary Search.
. Debugging with Timed Automata Mutations.
