Abstract This paper proposes a new method of combining SAT with discrete event simulation. This new integration proved useful for designing a solver for capacity analysis in early phase railway construction design. Railway capacity is complex to define and analyze, and existing tools and methods used in practice require comprehensive models of the railway network and its timetables. Design engineers working within the limited scope of construction projects report that only ad-hoc, experience-based methods of capacity analysis are available to them. Designs often have subtle capacity pitfalls which are discovered too late, only when network-wide timetables are made—there is a mismatch between the scope of construction projects and the scope of capacity analysis, as currently practiced. We suggest a language for capacity specifications suited for construction projects, expressing properties such as running time, train frequency, overtaking and crossing. Such specifications can be used as contracts in the interface between construction projects and network-wide capacity analysis. We show how these properties can be verified fully automatically by building a special-purpose solver which splits the problem into two: an abstracted SAT-based dispatch planning, and a continuous-domain dynamics with timing constraints evaluated using discrete event simulation. The two components communicate in a CEGAR loop (counterexample-guided abstraction refinement). This architecture is beneficial because it clearly distinguishes the combinatorial choices on the one hand from continuous calculations on the other, so that the simulation can be extended by relevant details as needed. We describe how loops in the infrastructure can be handled to eliminate repeating dispatch plans, and use case studies based on data from existing infrastructure and ongoing construction projects to show that our method is fast enough at relevant scales to provide agile verification in a design setting. Similar SAT modulo discrete event simulation combinations could also be useful elsewhere where one or both of these methods are already applicable such as in bioinformatics or hardware/software verification.

Data races are often discussed in the context of lock acquisition and release, with race-detection algorithms routinely relying on vector clocks as a means of capturing the relative ordering of events from different threads. In this paper, we present a data-race detector for a language with channel communication as its sole synchronization primitive, and provide a semantics directly tied to the happens-before relation, thus forging the notion of vector clocks.

This paper formalizes the observable interface behaviour ofopensystems for a strongly-typed, concurrent object-oriented language with single-class inheritance. We formally characterize the observable behaviour in terms of interactions at the program-environment interface. The behaviour is given by transitions between contextual judgments, where the absent environment is represented abstractly as assumption context. A particular challenge is the fact that, when the system is considered as open, code from the environment can be inherited to the component and vice versa. This requires to incorporate an abstract version of the heap into the environment assumptions when characterizing the interface behaviour. We prove the soundness of the abstract interface description.

The Uruguayan e-government agency has made available an Interoperability Platform (InP) with the purpose of facilitating the implementation of e-government services. By leveraging the Web Services technology, public agencies have implemented various atomic services which are usually hosted at the agencies but have to be accessed through proxy services in the InP. Given that the implementation of e-government processes involves invoking multiple services, the mechanisms to implement service orchestrations are increasingly required. Although there are well-known solutions for orchestrating Web Services, their application within the InP presents challenges, in particular, regarding the integration with its Security System. This paper proposes alternatives for implementing orchestrations of secure Web Services within the InP. The proposal consists of a base architecture that can be configured to implement different solution alternatives, enabling its application in other similar scenarios. The proposal was completely prototyped which allowed evaluating some operational aspects of the solution.

This paper extends our behavioural type and effect system for detecting deadlocks by polymorphism and formalizing type inference (with respect to lock types). Our inference is defined for a simple concurrent, first-order language. From the inferred effects, after suitable abstractions to keep the state space finite, we either obtain the verdict that the program will not deadlock, or that it may deadlock. We show soundness and completeness of the type inference.

The study of gene function is critical in various genomic and proteomic fields. Due to the availability of tremendous amounts of different types of protein data, integrating these datasets to predict function has become a significant opportunity in computational biology. In this paper, to predict protein function we (i) develop a novel Bayesian framework combining relational,hierarchical and structural information with improvement in data usage efficiency over similar methods, and (ii) propose to use it in conjunction with an integrative protein-protein association network, STRING (Search Tool for the Retrieval of INteracting Genes/proteins), which combines information from seven different sources. At the heart of our work is accomplishing protein data integration in a concerted fashion with respect to algorithm and data source. Method performance is assessed by a 5-fold cross-validation in yeast on selected terms from the Molecular Function ontology in the Gene Ontology database. Results show that our combined use of the proposed computational framework and the protein network from STRING offers substantial improvements in prediction. The benefits of using an aggressively integrative network, such as STRING, may derive from the fact that although it is likely that the ultimate gene interaction matrix (including but not limited to protein-protein, genetic, or regulatory interactions) will be sparse, presently it is still known only incompletely in most organisms, and thus the use of multiple distinct data sources is rewarded.

BACKGROUND: In the current climate of high-throughput computational biology, the inference of a protein's function from related measurements, such as protein-protein interaction relations, has become a canonical task. Most existing technologies pursue this task as a classification problem, on a term-by-term basis, for each term in a database, such as the Gene Ontology (GO) database, a popular rigorous vocabulary for biological functions. However, ontology structures are essentially hierarchies, with certain top to bottom annotation rules which protein function predictions should in principle follow. Currently, the most common approach to imposing these hierarchical constraints on network-based classifiers is through the use of transitive closure to predictions. RESULTS: We propose a probabilistic framework to integrate information in relational data, in the form of a protein-protein interaction network, and a hierarchically structured database of terms, in the form of the GO database, for the purpose of protein function prediction. At the heart of our framework is a factorization of local neighborhood information in the protein-protein interaction network across successive ancestral terms in the GO hierarchy. We introduce a classifier within this framework, with computationally efficient implementation, that produces GO-term predictions that naturally obey a hierarchical 'true-path' consistency from root to leaves, without the need for further post-processing. CONCLUSION: A cross-validation study, using data from the yeast Saccharomyces cerevisiae, shows our method offers substantial improvements over both standard 'guilt-by-association' (i.e., Nearest-Neighbor) and more refined Markov random field methods, whether in their original form or when post-processed to artificially impose 'true-path' consistency. Further analysis of the results indicates that these improvements are associated with increased predictive capabilities (i.e., increased positive predictive value), and that this increase is consistent uniformly with GO-term depth. Additional in silico validation on a collection of new annotations recently added to GO confirms the advantages suggested by the cross-validation study. Taken as a whole, our results show that a hierarchical approach to network-based protein function prediction, that exploits the ontological structure of protein annotation databases in a principled manner, can offer substantial advantages over the successive application of 'flat' network-based methods.

Formal methods, especially model checking, are an indispensable part of the software engineering process. With large software systems currently beyond the range of fully automatic verification, however, a combination of decomposition and abstraction techniques is needed. To model check components of a system, a standard approach is to close the component with an abstraction of its environment. To make it useful in practice, the closing of the component should be automatic, both for data and for control abstraction. Specifically for model checking asynchronous open systems, external input queues should be removed, as they are a potential source of a combinatorial state explosion. In this paper we close a component synchronously by embedding the external environment directly into the system to avoid the external queues, while for the data, we use a two-valued abstraction, namely data influenced from the outside or not. This gives a more precise analysis than that investigated by Ioustinova et al. (2002). To further combat the state explosion problem, we combine this data abstraction with a static analysis to remove superfluous code fragments. The static analysis we use is reminiscent of that presented by Ioustinova et al., but we use a combination of a may and a must-analysis instead of a may-analysis.

BACKGROUND: Intracellular signal transduction is achieved by networks of proteins and small molecules that transmit information from the cell surface to the nucleus, where they ultimately effect transcriptional changes. Understanding the mechanisms cells use to accomplish this important process requires a detailed molecular description of the networks involved. RESULTS: We have developed a computational approach for generating static models of signal transduction networks which utilizes protein-interaction maps generated from large-scale two-hybrid screens and expression profiles from DNA microarrays. Networks are determined entirely by integrating protein-protein interaction data with microarray expression data, without prior knowledge of any pathway intermediates. In effect, this is equivalent to extracting subnetworks of the protein interaction dataset whose members have the most correlated expression profiles. CONCLUSION: We show that our technique accurately reconstructs MAP Kinase signaling networks in Saccharomyces cerevisiae. This approach should enhance our ability to model signaling networks and to discover new components of known networks. More generally, it provides a method for synthesizing molecular data, either individual transcript abundance measurements or pairwise protein interactions, into higher level structures, such as pathways and networks.

Combining discrete state-machines with continuous behavior, hybrid systems are a well-established mathematical model for discrete systems acting in a continuous environment. As a priori infinite state systems, their computational properties are undecidable in the general model and the main line of research concentrates on model checking of finite abstractions of restricted subclasses of the general model. In our work, we use deductive methods, falling back upon the general-purpose theorem prover PVS. To do so we extend the classical approach for the verification of state-based programs by developing an inductive proof method to deal with the parallel composition of hybrid systems. It covers shared variable communication, label-synchronization, and especially the common continuous activities in the parallel composition of hybrid automata. Besides hybrid systems and their parallel composition, we formalized their operational step semantics and a number of proof-rules within PVS, for one of which we give also a rigorous completeness proof. Moreover the theory is applied to the verification of a number of examples.

We report on a model checking case study of an industrial medium access protocol for wireless ATM. Since the protocol is too large to be verified by any of the existing checkers as a whole, the verification exploits the layered and modular structure of the protocol's SDL specification and proceeds in a bottom-up, compositional way. The compositional arguments are used in combination with abstraction techniques to further reduce the state space of the system. The verification is primarily aimed at debugging the system. After correcting the specification step by step and validating various untimed and time-dependent properties, a model of the whole control component of the medium-access protocol is built and verified. The significance of the case study is in demonstrating that verification tools can handle complex properties of a model as large as shown.