1,721,111 research outputs found
Restful services and web-os middleware: A formal specification approach
No full textWeb Operating Systems can be seen as an extension of traditional Operating Systems where the addresses used to manage files and execute programs (via the basic load/execution mechanism) are extended from local filesystem path-names to URLs. A first consequence is that, similarly as for traditional web technologies, executing a program at a given URL can be done in two modalities: either the execution is performed client-side at the invoking machine (and relative URL addressing in the executed program set to refer to the invoked URL) or it is performed server-side at the machine addressed by the invoked URL (as, e.g., for a web service). Moreover in this context, user identification for access to programs and files and workflow-based composition of service programs is naturally based on token/session-like mechanisms. We propose a middleware based on client-server protocols and on a set primitives for managing files/resources and executing programs (in the form of client-side/server-side components) in Web Operating Systems. The middleware is based on an extension of the REST architecture. In order to provide an unambiguous specification, we formally define the semantics of the proposed middleware by first introducing a process algebra for standard REST and then extending it to the whole middleware
Performance Measure Sensitive Congruences for Markovian Process Algebras
No full textThe modeling and analysis experience with process algebras has shown the necessity of extending them with priority, probabilistic internal/external choice, and time while preserving compositionality. The purpose of this paper is to make a further step by introducing a way to express performance measures, in order to allow the modeler to capture the QoS metrics of interest. We show that the standard technique of expressing stationary and transient performance measures as weighted sums of state probabilities and transition frequencies can be imported in the process algebra framework. Technically speaking, if we denote by n the number of performance measures of interest, in this paper we define a family of extended Markovian process algebras with generative master-reactive slaves synchronization mechanism called EMPAgr,n including probabilities, priorities, exponentially distributed durations, and sequences of rewards of length n. Then we show that the Markovian bisimulation equivalence ~MB,n is a congruence for EMPAgr,n which preserves the specified performance measures and we give a sound and complete axiomatization for finite EMPAgr,n terms. Finally, we present a case study conducted with the software tool TwoTowers in which we contrast the average performance of a selection of distributed algorithms for mutual exclusion modeled with EMPAgr,n
Guest Editorial: Special Issue on Service-Oriented Architectures and Programming
No full textThis special issue includes revised versions of selected papers that were presented at the Special Track
on Service-Oriented Architectures and Programming (SOAP) of the 29th Annual ACM Symposium on
Applied Computing (SAC 2014). SOAP 2014 was held in Gyeongju, Korea, in March 24-28, 2014. Its proceedings were published in a volume edited by Yookun Cho, Sung Y. Shin, Sang-Wook Kim, Chih-Cheng Hung and Jiman Hong and published by ACM in 2014. This special issue was motivated by the quality of the works presented at the conference and by the increasing proliferation of service-oriented systems in our society such as e-governance, e-health and e-commerce systems. We believe that the contributions in this volume provide a valuable example of
current research in this area. We also believe that the published works will contribute to the main aims of
the SOAP track, that is to transform Service-Oriented Programming (SOP) into a mature discipline with
both solid scientific foundations and mature software engineering development methodologies supported
by dedicated tools
Introduction to the Software Engineering and Formal Methods 2013 special issue
No full textWe are in the world in which society is increasingly dependent
on software, and so, the quality of this software is
more important than ever. Unfortunately, the development of
high-quality software is becoming increasingly challenging
as complexity grows and systems are often concurrent and
distributed. The Software Engineering and Formal Methods
communities have developed a range of approaches that help
address this problem, but initially there was relatively little
interaction between these areas and some saw them as rivals.
Thankfully, these attitudes have gradually changed, with the
communities accepting that each makes a useful contribution
in tackling an important problem.
It is arguable that several factors have helped bring
together the Software Engineering and Formal Methods communities.
For example, there has been increasing interest in
topics such as model-based testing that fall within both areas,
and so, there is much more overlap between the communities.
Recent years have seen increases in computation power
and improvements in solution mechanisms such as SAT/SMT
solvers and model checkers. This has led to verification and
static analysis techniques, developed in the formal methods
community, scaling to much larger systems and being used by
many more software engineers. However, events that bring
these communities together have also played a crucial role
Reward based congruences: Can we aggregate more
No full textIn this paper we extend a performance measure sensitive Markovian bisimulation congruence based on yield and bonus rewards that has been previously defined in the literature, in order to aggregate more states and transitions while preserving compositionality and the values of the performance measures. The extension is twofold. First, we show how to define a performance measure sensitive Markovian bisimulation congruence that aggregates bonus rewards besides yield rewards. This is achieved by taking into account in the aggregation process the conditional execution probabilities of the transitions to which the bonus rewards are attached. Second, we show how to define a performance measure sensitive Markovian bisimulation congruence that allows yield rewards and bonus rewards to be used interchangeably up to suitable correcting factors, aiming at the introduction of a normal form for rewards. We demonstrate that this is possible in the continuous time case, while it is not possible in the discrete time case because compositionality is lost
Compositional Asymmetric Cooperations for Process Algebras with Probabilities, Priorities, and Time
No full textThe modeling and analysis experience with process algebras has shown the necessity of extending them with priority, probabilistic internal/external choice, and time in order to be able to faithfully model the behavior of real systems and capture the properties of interest. An important open problem in this scenario is how to obtain semantic compositionality in the presence of all these mechanisms, to allow for an efficient analysis. In this paper we argue that, when abandoning the classical nondeterministic setting by considering the mechanisms above, a natural solution is to break the symmetry of the roles of the processes participating in a synchronization. We accomplish this by distinguishing between master actions – the choice among which is carried out generatively according to their priorities/probabilities or exponentially distributed durations – and slave actions – the choice among which is carried out reactively according to their priorities/probabilities – and by imposing that a master action can synchronize with slave actions only. Technically speaking, in this paper we define a process algebra called EMPAgr including probabilities, priorities, exponentially distributed durations, and the generative master-reactive slaves synchronization mechanism. Then, we prove that the synchronization mechanism in EMPAgr is correct w.r.t. the novel cooperation structure model, we show that the Markovian bisimulation equivalence is a congruence for EMPAgr, and we present a sound and complete axiomatization for finite terms
Fair Asynchronous Session Subtyping
Full text linkSession types are widely used as abstractions of asynchronous message passing systems. Refinement for such abstractions is crucial as it allows improvements of a given component without compromising its compatibility with the rest of the system. In the context of session types, the most general notion of refinement is asynchronous session subtyping, which allows message emissions to be anticipated w.r.t. a bounded amount of message consumptions. In this paper we investigate the possibility to anticipate emissions w.r.t. an unbounded amount of consumptions: to this aim we propose to consider fair compliance over asynchronous session types and fair refinement as the relation that preserves it. This allows us to propose a novel variant of session subtyping that leverages the notion of controllability from service contract theory and that is a sound characterisation of fair refinement. In addition, we show that both fair refinement and our novel subtyping are undecidable. We also present a sound algorithm which deals with examples that feature potentially unbounded buffering. Finally, we present an implementation of our algorithm and an empirical evaluation of it on synthetic benchmarks
Functional and Performance Modeling and Analysis of Token Ring Using EMPA
No full textWe present an application of the integrated approach based on the stochastically timed process algebra EMPA to the analysis of token ring. The protocol is formally represented in EMPA. The deadlock freeness of the protocol and the utilization of the channel are then assessed by automatically analyzing the algebraic description with the EMPA based software tool TwoTowers. Finally, we show the potentialities of the integrated approach by investigating the fairness of the protocol, which depends on both functional and performance aspects
Towards Dynamic Updates in Service Composition
Full text linkInternational audienceWe survey our work on choreographies and behavioural contracts in multiparty interactions. In particular theories of behavioural contracts are presented which enable reasoning about correct service composition (contract compliance) and service substitutability (contract refinement preorder) under different assumptions concerning service communication: synchronous communication with patient non-preemptable or impatient invocations, or asynchronous communication. Correspondingly, relations concerning behavioural contracts and choreographic descriptions are considered, where a contract for each communicating party is, e.g., derived by projection.Contract refinement relations are induced as the maximal preoders which preserve contract compliance and global traces. The obtained preorders are then characterized in terms of a new form of testing, called compliance testing (where not only tests must succeed but also the system under test), and compared with classical preorders. Moreover, recent work about adaptable choreographies and behavioural contracts is presented, where the theory above is extended to update mechanisms allowing choreographies/contracts to be modified at run-time by internal (self-adaptation) or external intervention
- …
