Sophia-Antipolis, 2017 Sept 12.
Robert de Simone:
Title: On the relation between Concurrent Models of Computation and Communication and Parallel Programming languages.
Abstract: Theoretical concurrent Models of Computation and Communication (such as Process Networks and Process Algebras), and practical Parallel Programming Models (such as MPI, OpenMP, OpenCL) are means to describe application structure meant to promote parallel execution on relevant architectures. Nevertheless, their underlying notions hardly match, and this mismatch between prevalent theory and practice negatively impacts, in our view, the possibility of parallel optimization. We investigate the design of a new MoCC, inspired from existing ones, but adding features that lead to a closer relation with existing PPMs.
Min Zhang (M)
Title: A unified framework for formal reasoning of clock constraints using satisfiability solving
Abstract: CCSL (abbreviated for Clock Constraint Specification Language) is an emerging formal language for specifying the constraints between the occurrences of events in real-time embedded systems. The role that such constraints play in the design is that constraints are supposed to satisfy system requirements, and meanwhile a real-time embedded system being designed is supposed to satisfy all the constraints. Many approaches have been proposed to formal analysis of such satisfiabilities for CCSL. Most of the existing approaches are either ad-hoc, e.g., for model checking or simulation, or not scalable. In this talk, I will introduce a unified framework for formal reasoning of CCSL using satisfiability solving technique. The framework is unified in that it makes use of state-of-the-art SMT solvers such as Z3 and CVC4 to formally analyze CCSL constraints by means of bounded model checking, theorem proving, and trace analysis. For the efficiency of SMT solvers, the proposed approach is scalable to complex systems. Experimental results demonstrate both the effectiveness and the efficiency of our approach.
Frederic Mallet:
Title: Model-Based System Engineering for Cyber-Physical Systems
Abstract: Cyber-Physical Systems (CPSs) are networks of heterogeneous embedded systems immersed within a physical environment. Several ad-hoc frameworks and mathematical models have been studied to deal with challenging issues raised by CPSs. We explore a more standard-based approach that relies on UML/SysML/MARTE to capture different aspects of CPSs, including structure, system behaviors, clock constraints, and non-functional properties. The novelty of our work lies in the use
of logical clocks and MARTE/CCSL to drive and coordinate different models. Meanwhile, to capture stochastic behaviors of CPSs, we propose an extension of CCSL, called pCCSL, where logical clocks are adorned with stochastic properties. The stochastic information is used to capture the uncertain behavior of the environment. Possible variants are explored using Statistical Model Checking (SMC) via a transformation from the MARTE/pCCSL models into Stochastic Hybrid Automata. The whole process is illustrated through a case study of energy-aware building in which the system is modeled by UML/MARTE/pCCSL and different variants are explored through SMC to help expose the best alternative solutions.
Yuxin Deng (presented by Min Zhang (F))
Title: Logical Characterizations of Probabilistic Bisimilarity
Abstract:
For labeled Markov processes with continuous state space, van Breugel et al. provided a remarkable modal logic to characterize probabilistic bisimilarity without employing any modality indexed with numbers. The proof of this elegant characterization employs advanced machinery on topology theory. In the discrete case of finite-state probabilistic processes, we prove that result with an elementary and more accessible proof. Moreover, our proof is constructive.
Ludovic HENRIO:
Title: An Overview of Active-object Languages
Abstract: To program parallel systems efficiently and easily, a wide range of programming models appeared, each with different choices concerning synchronization and communication between parallel entities. Among them, the actor model is based on loosely coupled parallel entities that communicate through asynchronous messages thanks to the use of mailboxes. Some actor languages provide a strong integration with the object-oriented concepts; they are often called active object languages. This talk reviews the principles of actor and active object languages and compares them according to well-chosen aspects that cover the programming paradigms and their implementation.
Min Zhang (F)
Title: The transition and properties from Boolean networks to Discrete-time Markov Chains：A case study of mice stem cell gene regulatory networks
Abstract: This paper proposes a new method based on probabilistic model checking technique to solve the problem of detecting attractors in gene regulatory networks which is vital in bioengineering. We transform a gene regulatory network into a Discrete-time Markov Chains (DTMC for short) by using truth table. We verify the possibility of gene activation in some “long term” through a model checker named PRISM, which help us to find attractors of the gene regulatory network. In this paper, we show the whole procedure using the example of mice stem cell gene regulatory networks. Meanwhile, we make a new technique of detecting the promotion/inhibition relations between genes by adding gene disturbance and modifying gene activation/suppression probability. We show that in the mice regulatory network, seven genes will remain their invariable states in some” long term”, then the rest of “changing” genes forms a cyclic attractor. The experiment shows that our method can easily and directly to find the attractors. Moreover, our experiment successfully finds those genes affected by gene Gata1, which would be helpful for studying of the mice leucopenia.
Eric Madelaine:
Title: A Theory for the Composition of Concurrent Processes: Towards algorithms and tools.
Abstract: We provide a theory for the operators composing concurrent processes. Open pNets (parameterized networks of synchronized automata) are new semantic objects that we propose for defining the semantics of composition operators. We define the operational semantics of open pNets, using “open transitions” that include symbolic hypotheses on the behavior of the pNets “holes”. We discuss when this semantics can be finite and how to compute it symbolically. We have implemented a prototype algorithm for building the semantics of an Open pNet. This state-generation algorithm contains a classical part based on finite-state automata, but also a SMT solver (here Z3), used to check satisfiability and inclusion of predicates over action expressions. We illustrate the approach on examples taken from various process languages, and propose a number of challenges as perspectives. We show a new case study based on a BIP specification of the onboard software of nano-satellites.
Recent Comments