Search

In this paper we explore the combination of novel spatio-temporal model-checking techniques, and of a recently developed model-based approach to the study of bike sharing systems, in order to detect, visualize and investigate potential problems with bike sharing system configurations. In particular the formation and dynamics of clusters of full stations is explored. Such clusters are likely to be related to the difficulties of users to find suitable parking places for their hired bikes and show up as surprisingly long cycling trips in the trip duration statistics of real bike sharing systems of both small and large cities. Spatio- temporal analysis of the pattern formation may help to explain the phenomenon and possibly lead to alternative bike repositioning strategies aiming at the reduction of the size of such clusters and improving the quality of service.

Part 1: Tuple-Based Coordination; International audience; Recently, there has been growing interest in nature-inspired interaction paradigms for Collective Adaptive Systems, for modelling and implementation of adaptive and context-aware coordination, among which the promising pheromone-based interaction paradigm. System modelling in the context of such a paradigm may be facilitated by the use of languages in which adaptive interaction is decoupled in time and space through asynchronous buffered communication, e.g. asynchronous, repository- or tuple-based languages. In this paper we propose a differential semantics for such languages. In particular, we consider an asynchronous, repository based modelling kernel-language which is a restricted version of LINDA, extended with stochastic information about action duration. We provide stochastic formal semantics for both an agent-based view and a population-based view. We then derive an ordinary differential equation semantics from the latter, which provides a fluid-flow deterministic approximation for the mean behaviour of large populations. We show the application of the language and the ODE analysis on a benchmark example of foraging ants.

Public bike-sharing systems are a popular means of sustainable urban mobility, but their successful introduction in a city stands or falls with their specific designs. What kind of bikes and docking stations are needed, how many and where to install them? How to avoid as much as possible that stations are completely empty or full for some period? Hence, a bike-sharing system can be seen both as a highly (re)configurable system and as a collective adaptive system. In this paper, we present two complementary strategies for the evaluation of bike-sharing system designs by means of automated tool support. We use the Clafer toolset to perform multi-objective optimisation of attributed feature models known from software product line engineering and the recently developed mean field model checker FlyFast to assess performance and user satisfaction aspects of variants of large-scale bike-sharing systems. The combined use of these analysis approaches is a preliminary step in the direction of automatic decision support for the initial design of a bike-sharing system as well as its successive adaptations and reconfigurations that considers both qualitative and performance aspects.

In this work we present a spatial extension of the global model checking algorithm of the temporal logic CTL. This classical veri- fication framework is augmented with ideas coming from the tradition of topological spatial logics. More precisely, we add to CTL the operators of the Spatial Logic of Closure Spaces, including the surrounded operator, with its intended meaning of a point being surrounded by entities sat- isfying a specific property. The interplay of space and time permits one to define complex spatio-temporal properties. The model checking algo- rithm that we propose features no particular efficiency optimisations, as it is meant to be a reference specification of a family of more efficient algorithms that are planned for future work. Its complexity depends on the product of temporal states and points of the space. Nevertheless, a prototype model checker has been implemented, made available, and used for experimentation of the application of spatio-temporal verifica- tion in the field of collective adaptive systems.

Modelling of bike sharing systems as Markov Renewal Process is examined with the aim of capturing and assessing various forms of user (dis)satisfaction. A class of models with minimal assumptions about distributions of bicycle parking stations and service requests is developed in which rational commuter behaviour is taken into account. Stochastic time evolution of these models is studied, using a generalised version of Gillespie's exact stochastic integration algorithm that accounts for non-Markovian inter-event times. The model is shown to reproduce quite faithfully the trip-duration statistics of smaller and larger real bike sharing systems, such as those in London and Pisa, including the algebraic `tails' of these distributions that are made up of longer cycling trips. The latter are related to user's difficulties to find suitable parking places therefore to a potential source of distress. The model also predicts other salient features such as a mode at 10 minutes and crossover behaviour at about 30 minutes. The framework can be extended to include measures either designed to improve, or anyway to affect, the user experience with a system, such as incentives for spontaneous vehicle redistribution. User satisfaction is difficult to assess in real systems because these naturally collect only data about trips that actually, and thus successfully, took place giving only partial and biased insight into user satisfaction.

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.

A characteristic that many emerging technologies and interaction techniques have in common is a shift towards tighter coupling between human and computer. In addition to traditional discrete interaction, more continuous interaction techniques, such as gesture recognition, haptic feedback and animation, play an increasingly important role. Additionally, many supervisory control systems (such as flight deck systems) already have a strong continuous element. The complexity of these systems and the need for rigorous analysis of the human factors involved in their operation leads us to examine formal and possibly automated support for their analysis. The fact that these systems have important temporal aspects and potentially involve continuous variables, besides discrete events, motivates the application of hybrid systems modelling, which has the expressive power to encompass these issues. Essentially, we are concerned with human-factors related questions whose answers are dependent on interactions between the user and a complex, dynamic system. In this paper we explore the use of hybrid automata, a formalism for hybrid systems, for the specification and analysis of interactive systems. To illustrate the approach we apply it to the analysis of an existing flight deck instrument for monitoring and controlling the hydraulics subsystem.

A novel, scalable, on-the-fly model-checking procedure is presented to verify bounded PCTL properties of selected individuals in the context of very large systems of independent interacting objects. The proposed procedure combines on-the-fly model checking techniques with deterministic mean-field approximation in discrete time. The asymptotic correctness of the procedure is shown and some results of the application of a prototype implementation of the FlyFast model-checker are presented.

Model checking approaches can be divided into two broad categories: global approaches that determine the set of all states in a model M that satisfy a temporal logic formula f, and local approaches in which, given a state s in M, the procedure determines whether s satisfies f. When s is a term of a process language, the model checking procedure can be executed "on-the-fly", driven by the syntactical structure of s. For certain classes of systems, e.g. those composed of many parallel components, the local approach is preferable because, depending on the specific property, it may be sufficient to generate and inspect only a relatively small part of the state space. We propose an efficient, on-the-fly, PCTL model checking procedure that is parametric with respect to the semantic interpretation of the language. The procedure comprises both bounded and unbounded until modalities. The correctness of the procedure is shown and its efficiency is compared with a global PCTL model checker on representative applications., Comment: In Proceedings ICE 2014, arXiv:1410.7013

Predicate-based communication allows components of a system to send messages and requests to ensembles of components that are determined at execution time through the evaluation of a predicate, in a multicast fashion. Predicate-based communication can greatly simplify the programming of autonomous and adaptive systems. We present a stochastically timed extension of the Software Component Ensemble Language (SCEL) that was introduced in previous work. Such an extension raises a number of non-trivial design and formal semantics issues with different options as possible solutions at different levels of abstraction. We discuss four of these options, of which two in more detail. We provide a formal semantics definition and an illustration of the use of the language modeling a bike sharing system, together with some preliminary analysis of the system performance., In Proceedings QAPL 2014, arXiv:1406.1567

This chapter contains sections titled: Introduction thinkteam Analysis of the thinkteam Log File thinkteam with Replicated Vaults Lessons Learned Conclusions Acknowledgments References

Workers of the Argentine ant, Iridomyrmex humilis, are known to be capable to find efficiently the shortest route from their nest to a food source. Their approach is based on a simple pheromone trail-laying and following behaviour accessing only local information. In this note we explore the modelling and analysis of foraging ants in Bio-PEPA [8,6]. The simple case study concerns ants that need to cross a bridge with two branches of different length to reach food and carry the food home and is based on empirical data described by Goss and Deneubourg et al. [13,10]. We explore the conditions for which the shortest path emerges as the preferred one by the ants. The analysis is based on stochastic simulation and fluid flow analysis. The behaviour of ant colonies has inspired the development of an interesting class of optimisation algorithms ranging from alternative shortest path algorithms to new scheduling and routing algorithms, algorithms to solve set partition problems and for distributed information retrieval. Process algebraic fluid flow analysis may be an important additional technique to the analysis of such algorithms in a computationally efficient way.

The Temporal Mobile Stochastic Logic (MoSL) has been introduced in previous works by the authors for formulating properties of systems specified in StoKlaim, a Markovian extension of Klaim. The main purpose of MoSL is addressing key functional aspects of network aware programming such as distribution awareness, mobility and security and to guarantee their integration with performance and dependability guarantees. In this paper we present SoSL, a variant of MoSL, designed for dealing with specific features of Service-Oriented Computing (SOC). We also show how SoSL formulae can be model-checked against systems descriptions expressed with MarCaSPiS, a process calculus designed for addressing quantitative aspects of SOC. In order to perform actual model checking, we rely on a dedicated front-end that uses existing state-based stochastic model-checkers, like e.g. the Markov Reward Model Checker (MRMC).

In this paper we show how Rate Transition Systems (RTSs ) can be used as a unifying framework for the definition of the semantics of stochastic process algebras. RTSs facilitate the compositional definition of such semantics exploiting operators on the next state functions which are the functional counterpart of classical process algebra operators. We apply this framework to representative fragments of major stochastic process calculi namely TIPP , PEPA and IML and show how they solve the issue of transition multiplicity in a simple and elegant way. We, moreover, show how RTSs help describing different languages, their differences and their similarities. For each calculus, we also show the formal correspondence between the RTSs semantics and the standard SOS one.

This paper presents an approach for investigating in a predictive way potential disruptive effects of interruptions on task performance in a multitasking environment. The approach combines previous work in the field of interruption analysis, formal description techniques for interactive systems and stochastic processes to support performance analysis of user activities constrained by the occurrence of interruptions. The approach uses formal description techniques to provide a precise description of user tasks, and both system and interruptions behavior. The detailed mechanism by which systems and interruptions behave is first described using a Petri nets-based formal description technique called Interactive Cooperative Objects (ICO). The use of a formal modeling technique for the description of these three components makes it possible to compare and analyze different interaction techniques. In particular, it allows us to determine which of the system states are most affected by the occurrence of interruptions. Once composed together, models describing the system, user tasks and interruptions behavior are transformed into PEPA models (i.e. Performance Evaluation Process Algebra) that are amenable to performance analysis using the PRISM model checker. The approach is exemplified by a simple example that models two interaction techniques for manipulating icons in a desktop environment.

The definition of behavioural preorders over process terms as the maximal (pre-)congruences induced by basic observables has proven to be a useful technique to define various preorders and equivalences in the non-probabilistic setting. In this paper, we consider probabilistic observables to define an observational semantics for a probabilistic process calculus. The resulting pre-congruence is proven to coincide with a probabilistic may preorder, which, in turn, corresponds to a natural probabilistic extension of the may testing preorder of De Nicola and Hennessy.

In this paper an extension of a behavioural subset of UML statecharts for mobile computations is proposed. We study collections of UML objects whose behaviour is given by statecharts. Each object resides in a given place, and a collection of such places forms a network. Objects are aware of the localities of other objects, i.e. the logical names of the places where the latter reside, but not of the physical name of such places. In addition to their usual capabilities, such as sending messages etc., objects can move between places and create and destroy places, which may result in a deep reconfiguration of the network. A formal semantics is presented for this mobility extension which builds upon a core semantics definition of statecharts without mobility which we have used successfully in several contexts in the past years. An example of a model of a network service which exploits mobility for resource usage balance is provided using the proposed extension of UML statecharts.

Free flight has been proposed as a future alternative to the current policy in air traffic management (ATM) where aircraft follow predefined corridors. In free flight pilots can choose their own optimal routes, altitudes and velocities but are also responsible for the safe and fair resolution of trajectory conflicts. This would require a safe distributed control system were the trajectories that aircraft follow are as optimal as possible respecting sufficient safety distances. We model aircraft behaviour using non-determinism in such a way that reachability analysis provides the optimal trajectories of the aircraft. We compare the obtained results with the conflict resolution solutions proposed in the literature.

We propose a formal testing framework for a behavioural subset of UML statechart diagrams (UMLSDs). A formal operational semantics is defined, which uses the same core semantics introduced in Latella et al. (1999) but which is better suited for testing theory. The new semantics is proved consistent with our original one and is guaranteed to generate only finite state machines. Proper testing pre-orders and equivalences are defined which allow us to equate/distinguish systems on the basis of their interaction with the surrounding environment, abstracting from their internal structure. Finally, we provide a way for effective automatic verification of testing equivalence of our statecharts, based on existing techniques and tools.

We present a stochastically timed extension of UML statechart diagrams. The extension is rather simple both from a notational point of view and from a semantics point of view. In particular we enrich a state/transition formal operational semantics we proposed in (Latella et al., 1999) with random clocks for expressing time values. We do this in an orthogonal way, which means that the enriched semantics preserves all the properties of the untimed one. We show, by means of a simple example, how the enriched notation and its semantics can be used for performing quantitative analysis of stochastic UML statechart diagram models.

Architecture-based approaches have been promoted as a means of controlling the complexity of system construction and evolution, in particular for providing systems with the agility required to operate in turbulent environments and to adapt very quickly to changes in the enterprise world. Recent technological advances in communication and distribution have made mobility an additional factor of complexity, one for which current architectural concepts and techniques can be hardly used. The AGILE project is developing an architectural approach in which mobility aspects can be modelled explicitly and mapped on the distribution and communication topology made available at physical levels. The whole approach is developed over a uniform mathematical framework based on graph-oriented techniques that support sound methodological principles, formal analysis, and refinement. This paper describes the AGILE project and some of the results gained during the first project year.

I:Selection of Papers Presented at 5thSPIN99.- Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving.- Runtime Efficient State Compaction in Spin.- Distributed-Memory Model Checking with SPIN.- Partial Order Reduction in Presence of Rendez-vous Communications with Unless Constructs and Weak Fairness.- Divide, Abstract, and Model-Check.- II: Papers Presented at 6thSPIN99.- Formal Methods Adoption: What's Working, What's Not!.- Model Checking for Managers.- Xspin/Project - Integrated Validation Management for Xspin.- Analyzing Mode Confusion via Model Checking.- Detecting Feature Interactions in the Terrestrial Trunked Radio (TETRA) Network Using Promela and Xspin.- Java PathFinder A Translator from Java to Promela.- VIP: A Visual Interface for Promela.- Events in Property Patterns.- Assume-Guarantee Model Checking of Software: A Comparative Case Study.- A Framework for Automatic Construction of Abstract Promela Models.- Model Checking Operator Procedures.- Applying Model Checking in Java Verification.- The Engineering of a Model Checker: the Gnu i-Protocol Case Study Revisited..- Embedding a Dialect of SDL in PROMELA.- dSPIN: A Dynamic Extension of SPIN.

Statechart Diagrams are a notation for describing behaviours in the framework of UML, the Unified Modeling Language of object-oriented systems. UML is a semi-formal language, with a precisely defined syntax and static semantics but with an only informally specified dynamic semantics. UML Statechart Diagrams differ from classical statecharts, as defined by Harel, for which formalizations and results are available in the literature. This paper sets the basis for the development of a formal semantics for UML Statechart Diagrams based on Kripke structures. This forms the first step towards model checking of UML Statechart Diagrams. We follow the approach proposed by Mikk and others: we first map Statechart Diagrams to the intermediate format of extended hierarchical automata and then we define an operational semantics for these automata. We prove a number of properties of such semantics which reflect the design choices of UML Statechart Diagrams.

Statechart diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modelling Language (UML). In this paper, we present a branching-time model-checking approach to the automatic verification of the formal correctness of UML Statechart diagram specifications. We use a formal operational semantics for building a labelled transition system (automaton) which is then used as a model to be checked against correctness requirements expressed in Action-Based Temporal Logic (ACTL). Our reference verification environment is JACK, where automata are represented in a standard format, which facilitates the use of different tools for automatic verification.

We present the formal specification and verification of a multimedia stream. The stream is described in a timed automata notation. We verify that the stream satisfies certain quality of service properties, in particular, throughput and end-to-end latency. The verification tool used is the real-time model checker UPPAAL.

User interfaces of many application systems have begun to include multiple devices which can be used together to input single expressions. Such interfaces (and even the whole application systems) are widely labelled multi-modal, since they use different types of communication channels to acquire information.

We report on a fruitful combination of applying academic experience with formal modelling and verification techniques to an industrial case study. The goal of the case study was to investigate a priori, i.e. before implementation, the effects of adding a lightweight and easy-to-use publish/subscribe (event) notification service to thinkteam/spl reg/ - an asynchronous and dispersed groupware system which was developed by think3. Researchers from the Formal Methods and Tools (FM&&T) group of ISTI-CNR $with a longstanding experience in research on the development and application of formal methods, notations, and software tools for the specification, design, and verification of complex computer systems - therefore teamed up with think3 - a global provider of integrated product development solutions that provides mechanical design and Product Data Management (PDM) software catering the product management needs of design processes in the manufacturing industry. The technical details of this joint research effort have been documented elsewhere, here we report on the lessons learned from this experience.

Part 6: Program Analysis; International audience; Smart contracts have been argued to be a means of building trust between parties by providing a self-executing equivalent of legal contracts. And yet, code does not always perform what it was originally intended to do, which resulted in losses of millions of dollars. Static verification of smart contracts is thus a pressing need. This paper presents an approach to verifying smart contracts written in Solidity by automatically translating Solidity into Java and using KeY, a deductive Java verification tool. In particular, we solve the problem of rolling back the effects of aborted transactions by exploiting KeY’s native support of JavaCard transactions. We apply our approach to a smart contract which automates a casino system, and discuss how the approach addresses a number of known shortcomings of smart contract development in Solidity.

Part 5: Verification; International audience; A business process is a collection of structured activities producing a particular product or software. BPMN is a workflow-based graphical notation for specifying business processes. Formally analyzing such processes is a crucial challenge in order to avoid erroneous executions of the corresponding software. In this paper, we focus on timed business processes where execution time can be associated to several BPMN constructs. We propose an encoding of timed business processes into the Maude language, which allows one to automatically verify several properties of interest on processes such as the maximum/minimum/av-erage execution time or the timed degree of parallelism that provides a valuable guide for the problem of resource allocation. The analysis is achieved using the rewriting-based tools available in Maude, which also provides other techniques (e.g., reachability analysis and model checking) for verifying BPMN specifications. We applied our approach on a large set of BPMN processes for evaluation purposes.

Part 4: Resource, Components and Information Flow; International audience; The major research in the resource management literature focuses primarily on two complementary sub-problems: (1) specification languages for formulating resource requests and (2) constraint problems modelling allocation and scheduling. Both directions assume the knowledge of the underlying platform architecture and the dependencies it induces on the usage of the various resources. In this paper, we bridge this gap by introducing constraint-flow nets (cfNets). A cfNet is defined by a set of resources and dependencies between them, each dependency having an associated constraint schema. The model is inspired by Petri nets, with resources corresponding to places and dependencies—to transitions. Given an architecture of dependent resources, an initial resource request is propagated through the dependencies. The generated constraints are then conjuncted into the global allocation constraint. We study the notion of conflicts in cfNets and prove that for conflict-free cfNets the global allocation constraint can be constructed unambiguously. Furthermore, we provide an SMT-based algorithm for conflict detection and discuss the use of priorities to dynamically resolve conflicts at run-time. Finally, we illustrate the use of cfNets on a case study inspired by the Kalray MPPA architecture.

Part 5: Verification; International audience; The client ${\mathsf {must}}$ preorder relates tests (clients) instead of processes (servers). The existing characterisation of this preorder is unsatisfactory for it relies on the notion of usable clients which, in turn, are defined using an existential quantification over the servers that ensure client satisfaction. In this paper we characterise the set of usable clients for finite-branching LTSs, and give a sound and complete decision procedure for it. We also provide a novel coinductive characterisation of the client preorder, which we use to argue that the preorder is decidable, thus positively answering the question opened in [3, 6].

Part 2: Languages and Tools; International audience; During the last decades a lot of coordination models and languages have been proposed in the literature. These approaches have proven that they can greatly improve the development of distributed applications that are now common. However, to be used by many developers , there is still a gap regarding the available tools. This paper details a set of tools that have been built to develop applications in LINC, a coordination environment rooted in Linda tuple spaces and Gamma chemical machine approaches. These tools allow developers to design better coordination rules, to monitor and update a running distributed application. The tools proposed here include design and debugging tools.

Part 2: Languages and Tools; International audience; Attribute-based communication provides a novel mechanism to dynamically select groups of communicating entities by relying on predicates over their exposed attributes. In this paper, we embed the basic primitives for attribute-based communication into the functional concurrent language Erlang to obtain what we call AErlang, for attribute Erlang. To evaluate our prototype in terms of performance overhead and scalability we consider solutions of the Stable Marriage Problem based on predicates over attributes and on the classical preference lists, and use them to compare the runtime performance of AErlang with those of Erlang and X10. The outcome of the comparison shows that the overhead introduced by the new communication primitives is acceptable, and our prototype can compete performance-wise with an ad-hoc parallel solution in X10.

With the constant increase in the number of interconnected devices in today networks, more and more computations can be described by spatial computing abstractions. In this context, distances can be estimated in a fully-distributed way by the so-called gradient self-organisation pattern: it is a basic building block also for large-scale system coordination, frequently used to broadcast information, forecast pointwise events, as carrier for distributed sensing, and as combinator for higher-level spatial structures. However, computing gradients is very problematic in a mutable environment: existing algorithms fail in reaching adequate trade offs between accuracy and reaction speed to environment changes. In this paper we introduce a new gradient algorithm, BIS (Bounded Information Speed) gradient, which uses time information to achieve a smooth and predictable reaction speed, which is proved optimal for algorithms following a single-path-communication strategy. Following a proposed methodology for empirical evaluation of performance of spatial computing algorithms, we evaluate BIS gradient and compare it with other approaches. We show that BIS achieves the best accuracy while keeping smoothness under control.

Part 4: Resource, Components and Information Flow; International audience; Information flow techniques typically classify information according to suitable security levels and enforce policies that are based on binary relations between individual levels, e.g., stating that information is allowed to flow from one level to another. We argue that some information flow properties of interest naturally require coordination patterns that involve sets of security levels rather than individual levels: some secret information could be safely disclosed to a set of confidential channels of incomparable security levels, with individual leaks considered instead illegal; a group of competing agencies might agree to disclose their secrets, with individual disclosures being undesired, etc. Motivated by this we propose a simple language for expressing information flow policies where the usual admitted flow relation between individual security levels is replaced by a relation between sets of security levels, thus allowing to capture coordinated flows of information. The flow of information is expressed in terms of causal dependencies and the satisfaction of a policy is defined with respect to an event structure that is assumed to capture the causal structure of system computations. We suggest applications to secret exchange protocols, program security and security architectures, and discuss the relation to classic notions of information flow control.

Part 3: Types; International audience; Behavioral contracts are abstract descriptions of the communications that clients and servers perform. Behavioral contracts come naturally equipped with a notion of compliance: when a client and a server follow compliant contracts, their interaction is guaranteed to progress or successfully complete. We study two extensions of contracts, dealing respectively with backtracking and with speculative execution. We show that the two extensions give rise to the same notion of compliance. As a consequence, they also give rise to the same subcontract relation, which determines when one server can be replaced by another preserving compliance. Moreover, compliance and subcontract relation are both decidable in polynomial time.

Part 5: Verification; International audience; Compatibility of components is an important issue in the quest for systems of systems that guarantee successful communications, free from message loss and indefinite waiting for inputs. In this paper, we investigate compatibility in the context of systems consisting of reactive components which may communicate through the synchronised execution of common actions. We model such systems in the team automata framework, which does not impose any a priori restrictions on the synchronisation policy followed to combine the components. We identify a family of representative synchronisation types based on the number of sending and receiving components participating in synchronisations. Then, we provide a generic procedure to derive, for each synchronisation type, requirements for receptiveness and for responsiveness of team automata that prevent that outputs are not accepted and inputs are not provided, respectively. Due to the genericity of our approach w.r.t. synchronisation policies, we can capture compatibility notions for various multi-component system models known from the literature.

Robustness is a standard correctness property which intuitively means that if the input to the program changes less than a fixed small amount then the output changes only slightly. This notion is useful in the analysis of rounding error for floating point programs because it helps to establish bounds on output errors introduced by both measurement errors and by floating point computation. Compositional methods often do not work since key constructs---like the conditional and the while-loop---are not robust. We propose a method for proving the robustness of a while-loop. This method is non-local in the sense that instead of breaking the analysis down to single lines of code, it checks certain global properties of its structure. We show the applicability of our method on two standard algorithms: the CORDIC computation of the cosine and Dijkstra's shortest path algorithm., Comment: QAPL - Tenth Workshop on Quantitative Aspects of Programming Languages (2012)

We demonstrate the modelling of opportunistic networks using the process algebra stochastic HYPE. Network traffic is modelled as continuous flows, contact between nodes in the network is modelled stochastically, and instantaneous decisions are modelled as discrete events. Our model describes a network of stationary video sensors with a mobile ferry which collects data from the sensors and delivers it to the base station. We consider different mobility models and different buffer sizes for the ferries. This case study illustrates the flexibility and expressive power of stochastic HYPE. We also discuss the software that enables us to describe stochastic HYPE models and simulate them., In Proceedings QAPL 2012, arXiv:1207.0559