Bio-PEPA: An Extension of the Process Algebra PEPA for Biochemical Networks

In this work we introduce Bio-PEPA, a process algebra for the modelling and the analysis of biochemical networks. It is a modification of PEPA to deal with some features of biological models, such as stoichiometry and the use of generic kinetic laws. Bio-PEPA may be seen as an intermediate, formal, compositional representation of biological systems, on which different kinds of analysis can be carried out. Finally, we show a representation of a model, concerning a simple genetic network, in the new language.     

Equivalences for a biological process algebra

This paper investigates Bio-PEPA, the stochastic process algebra for biological modelling developed by Ciocchetta and Hillston. It focuses on Bio-PEPA with levels where molecular counts are grouped or concentrations are discretised into a finite number of levels. Basic properties of well-defined Bio-PEPA systems are established after which equivalences used for the stochastic process algebra PEPA are considered for Bio-PEPA, and are shown to be identical for well-defined Bio-PEPA systems. Two new semantic equivalences parameterised by functions, called g-bisimilarity and weak g-bisimilarity are introduced. Different functions lead to different equivalences for Bio-PEPA. Congruence is shown for both forms of g-bisimilarity under certain reasonable conditions on the function and the use of these equivalences are demonstrated with a biologically-motivated example where two similar species are treated as a single species, and modelling of alternative pathways in the MAPK kinase signalling cascade.     

A semantic equivalence for Bio-PEPA based on discretisation of continuous values

Bio-PEPA is a process algebra for modelling biological systems. An important aspect of Bio-PEPA is the ability it provides to discretise concentrations resulting in a smaller, more manageable state space. The discretisation is based on a step size which determines the size of each discrete level and also the number of levels. This paper considers the relationship between two discretisations of the same Bio-PEPA model that differ only in the step size and hence the number of levels, by using the idea of equivalence from concurrency and process algebra. We present a novel behavioural semantic equivalence, compression bisimilarity, and investigate when this equates two discretisations of the same model and the circumstances in which this equivalence is a congruence with respect to the synchronisation operator.     

PEPA Queues: Capturing Customer Behaviour in Queueing Networks

Queueing network formalisms are very good at describing the spatial movement of customers, but typically poor at describing how customers change as they move through the network. We present the PEPA Queues formalism, which uses the popular stochastic process algebra PEPA to represent the individual state and behaviour of customers and servers. We offer a formal semantics for PEPA Queues, plus a direct translation to PEPA, allowing access to the existing tools for analysing PEPA models. Finally, we use the ipc/DNAmaca tool-chain to provide passage-time analysis of a dual Web server example.     

Timed Concurrent Constraint Programming for Analysing Biological Systems

In this paper we present our first approach to model and verify biological systems using ntcc, a concurrent constraint process calculus. We argue that the partial information constructs in ntcc can provide a suitable language for such systems. We also illustrate how ntcc may provide a unified framework for the analysis of biological systems, as they can be described, simulated and verified using the elements provided by the calculus.     

Product form solution for a class of PEPA models

The advantages of the compositional structure within the Markovian process algebra PEPA for model construction and simplification have already been demonstrated. In this paper we show that for some PEPA models this structure may also be used to advantage during the solution of the model. Several papers offering product form solutions of stochastic Petri nets have been published during the last 10 years. In [R. Boucherie, A characterisation of independence for competing Markov chains with applications to stochastic Petri nets, IEEE Trans. Software Engrg. 20 (7) (1994) 536–544], Boucherie showed that these solutions were a special case of a simple exclusion mechanism for the product process of a collection of Markov chains. The results presented in this paper take advantage of his observation. In particular we show that PEPA models that generate such processes may be readily identified and show how the product form solution may be obtained. Although developed here in the context of PEPA the results presented can be easily generalised to any of the other Markovian process algebra languages.     

一种基于进程代数的软件体系结构描述语言PEADL

对性能评价进程代数(PEPA)扩展,提出具有时序特征的随机进程代数(ESPA)。在此基础上进一步提出一种软件体系结构描述语言(PEADL)。介绍PEADL的语法和语义,并通过三层C/S结构应用系统展示PEADL的表述能力。     

Stochastic Modelling of Communication Protocols from Source Code

A major development in qualitative model checking was the jump to verifying properties of source code directly, rather than requiring a separately specified model. We describe and motivate similar extensions to quantitative / performance analyses, with particular emphasis on communication protocols. The central aim is to extract a stochastic model (in the PEPA language) from such source code. We construct a model compositionally, so that each function in the system corresponds to a sequential PEPA process. Such a process is derived by abstract interpretation over the state machine of a function, using interval abstraction to represent linear expressions of integer variables. We illustrate this by an analysis of a simple protocol.     

Analyzing partially-implemented real-time systems

Most analysis methods for real-time systems assume that all the components of the system are at roughly the same stage of development and can be expressed in a single notation, such as a specification or programming language. There are, however, many situations in which developers would benefit from tools that could analyze partially-implemented systems: those for which some components are given only as high-level specifications while others are fully implemented in a programming language. In this paper, we propose a method for analyzing such partially-implemented real-time systems. We consider real-time concurrent systems for which some components are implemented in Ada and some are partially specified using regular expressions and graphical interval logic (GIL), a real-time temporal logic. We show how to construct models of the partially-implemented systems that account for such properties as run-time overhead and scheduling of processes, yet support tractable analysis of nontrivial programs. The approach can be fully automated, and we illustrate it by analyzing a small example     

随机进程代数新技术综述

本文以PEPA语言为例,对近年来发展起来的随机进程代数的缓解状态空间爆炸问题的新技术做一个综述．     

Text Classification for Azerbaijani Language Using Machine Learning

Text classification systems will help to solve the text clustering problem in the Azerbaijani language. There are some text-classification applications for foreign languages, but we tried to build a newly developed system to solve this problem for the Azerbaijani language. Firstly, we tried to find out potential practice areas. The system will be useful in a lot of areas. It will be mostly used in news feed categorization. News websites can automatically categorize news into classes such as sports, business, education, science, etc. The system is also used in sentiment analysis for product reviews. For example, the company shares a photo of a new product on Facebook and the company receives a thousand comments for new products. The systems classify comments like positive or negative. The system can also be applied in recommended systems, spam filtering, etc. Various machine learning techniques such as Naive Bayes, SVM, Multi-layer Perceptron have been devised to solve the text classification problem in Azerbaijani language.     

Reasoning about non-immediate triggers in biological networks

Modeling molecular interactions in signalling networks is important from various perspectives such as predicting side effects of drugs, explaining unusual cellular behavior and drug and therapy design. Various formal languages have been proposed for representing and reasoning about molecular interactions. The interactions are modeled as triggered events in most of the approaches. The triggering of events is assumed to be immediate: once an interaction is triggered, it should occur immediately. Although working well for engineering systems, this assumption poses a serious problem in modeling biological systems. Our knowledge about biological systems is inherently incomplete, thus molecular interactions are constantly elaborated and refined at different granularity of abstraction. The model of immediate triggers can not consistently deal with this refinement. In this paper we propose an action language to address this problem. We show that the language allows for refinements of biological knowledge, although at a higher cost in terms of complexity.      

Grammatical inference in bioinformatics

Bioinformatics is an active research area aimed at developing intelligent systems for analyses of molecular biology. Many methods based on formal language theory, statistical theory, and learning theory have been developed for modeling and analyzing biological sequences such as DNA, RNA, and proteins. Especially, grammatical inference methods are expected to find some grammatical structures hidden in biological sequences. In this article, we give an overview of a series of our grammatical approaches to biological sequence analyses and related researches and focus on learning stochastic grammars from biological sequences and predicting their functions based on learned stochastic grammars.     

Opacity of discrete event systems and its applications

In this paper, we investigate opacity of discrete event systems. We define two types of opacities: strong opacity and weak opacity. Given a general observation mapping, a language is strongly opaque if all strings in the language are confused with some strings in another language and it is weakly opaque if some strings in the language are confused with some strings in another language. We show that security and privacy of computer systems and communication protocols can be investigated in terms of opacity. In particular, two important properties in security and privacy, namely anonymity and secrecy, can be studied as special cases of opacity. We also show that by properly specifying the languages and the observation mapping, three important properties of discrete event systems, namely observability, diagnosability, and detectability, can all be reformulated as opacity. Thus, opacity has a wide range of applications. Also in this paper we provide algorithms for checking strong opacity and weak opacity for systems described by regular languages and having a generalized projection as the observation mapping.     

Non-functional properties in the model-driven development of service-oriented systems

Systems based on the service-oriented architecture (SOA) principles have become an important cornerstone of the development of enterprise-scale software applications. They are characterized by separating functions into distinct software units, called services, which can be published, requested and dynamically combined in the production of business applications. Service-oriented systems (SOSs) promise high flexibility, improved maintainability, and simple re-use of functionality. Achieving these properties requires an understanding not only of the individual artifacts of the system but also their integration. In this context, non-functional aspects play an important role and should be analyzed and modeled as early as possible in the development cycle. In this paper, we discuss modeling of non-functional aspects of service-oriented systems, and the use of these models for analysis and deployment. Our contribution in this paper is threefold. First, we show how services and service compositions may be modeled in UML by using a profile for SOA (UML4SOA) and how non-functional properties of service-oriented systems can be represented using the non-functional extension of UML4SOA (UML4SOA-NFP) and the MARTE profile. This enables modeling of performance, security and reliable messaging. Second, we discuss formal analysis of models which respect this design, in particular we consider performance estimates and reliability analysis using the stochastically timed process algebra PEPA as the underlying analytical engine. Last but not least, our models are the source for the application of deployment mechanisms which comprise model-to-model and model-to-text transformations implemented in the framework VIATRA. All techniques presented in this work are illustrated by a running example from an eUniversity case study.     

Component aggregation for PEPA models: An approach based on approximate strong equivalence

Approximate aggregation for PEPA components involves the construction of a smaller component that approximates the behaviour of the original one. Such an approximation at the component level can be very efficient and it can also result in a considerable reduction of the state-space for the underlying continuous-time Markov chain. We propose an approximate PEPA component aggregation strategy that relies on an approximate form of strong equivalence. The notion of strong equivalence captures behavioural similarity between components of different size. This quality renders approximate strong equivalence appropriate as a criterion to aggregate the state-space of PEPA components. We compare our newly proposed approach with previous work on component aggregation, where only a part of the component behaviour has been used as a criterion for aggregation. Our method requires fewer assumptions regarding the form of the components, and is therefore readily applicable to a larger family of PEPA models.     

An efficient algorithm for aggregating PEPA models

Performance Evaluation Process Algebra (PEPA) is a formal language for performance modeling based on process algebra. It has previously been shown that, by using the process algebra apparatus, compact performance models can be derived which retain the essential behavioral characteristics of the modeled system. However, no efficient algorithm for this derivation was given. We present an efficient algorithm which recognizes and takes advantage of symmetries within the model and avoids unnecessary computation. The algorithm is illustrated by a multiprocessor example     

Validation of static properties in unified modeling language models for cyber physical systems

Cyber physical systems (CPSs) can be found nowadays in various fields of activity. The increased interest for these systems as evidenced by the large number of applications led to complex research regarding the most suitable methods for design and development. A promising solution for specification, visualization, and documentation of CPSs uses the Object Management Group (OMG) unified modeling language (UML). UML models allow an intuitive approach for embedded systems design, helping end-users to specify the requirements. However, the UML models are represented in an informal language. Therefore, it is difficult to verify the correctness and completeness of a system design. The object constraint language (OCL) was defined to add constraints to UML, but it is deficient in strict notations of mathematics and logic that permits rigorous analysis and reasoning about the specifications. In this paper, we investigated how CPS applications modeled using UML deployment diagrams could be formally expressed and verified. We used Z language constructs and prototype verification system (PVS) as formal verification tools. Considering some relevant case studies presented in the literature, we investigated the opportunity of using this approach for validation of static properties in CPS UML models.