Exogenous Probabilistic Computation Tree Logic

We define a logic EpCTL for reasoning about the evolution of probabilistic systems. System states correspond to probability distributions over classical states and the system evolution is modelled by probabilistic Kripke structures that capture both stochastic and non–deterministic transitions. The proposed logic is a temporal enrichment of Exogenous Probabilistic Propositional Logic (EPPL). The model-checking problem for EpCTL is analysed and the logic is compared with PCTL; the semantics of the former is defined in terms of probability distributions over sets of propositional symbols, whereas the latter is designed for reasoning about distributions over paths of possible behaviour. The intended application of the logic is as a specification formalism for properties of communication protocols, and security protocols in particular; to demonstrate this, we specify relevant security properties for a classical contract signing protocol and for the so–called quantum one–time pad.     

ReSpecT Nets: Towards an Analysis Methodology for ReSpecT Specifications

A key feature for infrastructures providing coordination services is the ability to define the behaviour of coordination abstractions according to the requirements identified at design-time. We take as a representative for this scenario the logic-based language ReSpecT (Reaction Specification Tuples), used to program the reactive behaviour of tuple centres. ReSpecT specifications are at the core of the engineering methodology underlying the TuCSoN infrastructure, and are therefore the “conceptual place” where formal methods can be fruitfully applied to guarantee relevant system properties.In this paper we introduce ReSpecT nets, a formalism that can be used to describe reactive behaviours that can succeed and fail, and that allows for an encoding to Petri nets with inhibitor arcs. ReSpecT nets are introduced to give a core model to a fragment of the ReSpecT language, and to pave the way for devising an analysis methodology including formal verification of safety and liveness properties. In particular, we provide a semantics to ReSpecT specifications through a mapping to ReSpecT nets. The potential of this approach for the analysis of ReSpecT specifications is discussed, presenting initial results for the analysis of safety properties.     

Proving operational termination of membership equational programs

Reasoning about the termination of equational programs in sophisticated equational languages such as Elan, Maude, OBJ, CafeOBJ, Haskell, and so on, requires support for advanced features such as evaluation strategies, rewriting modulo, use of extra variables in conditions, partiality, and expressive type systems (possibly including polymorphism and higher-order). However, many of those features are, at best, only partially supported by current term rewriting termination tools (for instance mu-term, C i ME, AProVE, TTT, Termptation, etc.) while they may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive membership equational programs and such termination tools, and prove the correctness of such transformations. We also discuss a prototype tool performing the transformations on Maude equational programs and sending the resulting transformed theories to some of the aforementioned standard termination tools.     

On requirement verification for evolving Statecharts specifications

Software development processes have been evolving from rigid, pre-specified, and sequential to incremental, and iterative. This evolution has been dictated by the need to accommodate evolving user requirements and reduce the delay between design decision and feedback from users. Formal verification techniques, however, have largely ignored this evolution and even when they made enormous improvements and found significant uses in practice, like in the case of model checking, they remained confined into the niches of safety-critical systems. Model checking verifies if a system’s model \(\mathcal{M}\) satisfies a set of requirements, formalized as a set of logic properties \(\Phi\) . Current model-checking approaches, however, implicitly rely on the assumption that both the complete model \(\mathcal{M}\) and the whole set of properties \(\Phi\) are fully specified when verification takes place. Very often, however, \(\mathcal{M}\) is subject to change because its development is iterative and its definition evolves through stages of incompleteness, where alternative design decisions are explored, typically to evaluate some quality trade-offs. Evolving systems specifications of this kind ask for novel verification approaches that tolerate incompleteness and support incremental analysis of alternative designs for certain functionalities. This is exactly the focus of this paper, which develops an incremental model-checking approach for evolving Statecharts. Statecharts have been chosen both because they are increasingly used in practice natively support model refinements.     

Virtual Organizations in Arigatoni

Arigatoni is a lightweight overlay network that deploys the Global Computing Paradigm over the Internet. Communication for over the behavioral units of the overlay is performed by a simple resource discovery protocol (RDP). Basic Global Computers Units (GC) can communicate by first registering to a brokering service and then by mutually asking and offering services.Colonies and communities are the main entities in the model. A colony is a simple virtual organization composed by exactly one leader and some set (possibly empty) of individuals. A community is a raw set of colonies and global computers (think it as a soup of colonies and global computer without a leader).We present an operational semantics via a labeled transition system, that describes the main operations necessary in the Arigatoni model to perform leader negotiation, joining/leaving a colony, linking two colonies and moving one GC from one colony to another. Our formalization results to be adequate w.r.t. the algorithm performing peer logging/delogging and colony aggregation.     

A Priority-Based Admission Control Scheme for Commercial Web Servers

This paper investigates into the performance and load management of web servers that are deployed in commercial websites. Such websites offer various services such as flight/hotel booking, online banking, stock trading, and product purchases among others. Customers are increasingly relying on these round-the-clock services which are easier and (generally) cheaper to order. However, such an increasing number of customers’ requests makes a greater demand on the web servers. This leads to web servers’ overload and the consequential provisioning of inadequate level of service. This paper addresses these issues and proposes an admission control scheme which is based on the class-based priority scheme that classifies customer’s requests into different classes. The proposed scheme is formally specified using \(\Pi \) -calculus and is implemented as a Java-based prototype system. The prototype system is used to simulate the behaviour of commercial website servers and to evaluate their performance in terms of response time, throughput, arrival rate, and the percentage of dropped requests. Experimental results demonstrate that the proposed scheme significantly improves the performance of high priority requests but without causing adverse effects on low priority requests.     

OXPath: A language for scalable data extraction, automation, and crawling on the deep web

The evolution of the web has outpaced itself: A growing wealth of information and increasingly sophisticated interfaces necessitate automated processing, yet existing automation and data extraction technologies have been overwhelmed by this very growth. To address this trend, we identify four key requirements for web data extraction, automation, and (focused) web crawling: (1) interact with sophisticated web application interfaces, (2) precisely capture the relevant data to be extracted, (3) scale with the number of visited pages, and (4) readily embed into existing web technologies. We introduce OXPath as an extension of XPath for interacting with web applications and extracting data thus revealed—matching all the above requirements. OXPath’s page-at-a-time evaluation guarantees memory use independent of the number of visited pages, yet remains polynomial in time. We experimentally validate the theoretical complexity and demonstrate that OXPath’s resource consumption is dominated by page rendering in the underlying browser. With an extensive study of sublanguages and properties of OXPath, we pinpoint the effect of specific features on evaluation performance. Our experiments show that OXPath outperforms existing commercial and academic data extraction tools by a wide margin.     

A Language for Verification and Manipulation of Web Documents: (Extended Abstract)

In this paper we develop the language theory underpinning the logical framework PLF. This language features lambda abstraction with patterns and application via pattern-matching. Reductions are allowed in patterns. The framework is particularly suited as a metalanguage for encoding rewriting logics and logical systems where proof terms have a special syntactic constraints, as in term rewriting systems, and rule-based languages. PLF is a conservative extension of the well-known Edinburgh Logical Framework LF. Because of sophisticated pattern matching facilities PLF is suitable for verification and manipulation of HXML documents.     

Stochastic Ambient Calculus

Mobile Ambients (MA) have acquired a fundamental role in modelling mobility in systems with mobile code and mobile devices, and in computation over administrative domains. We present the stochastic version of Mobile Ambients, called Stochastic Mobile Ambients (SMA), where we extend MA with time and probabilities. Inspired by previous models, PEPA and Sπ, we enhance the prefix of the capabilities with a rate and the ambient with a linear function that operates on the rates of processes executing inside it. The linear functions associated with ambients represent the delays that govern particular administrative domains. We derive performance measures from the labelled transition semantics as in standard models. We also define a strong Markov bisimulation in the style of reduction semantics known as barbed bisimulation. We argue that performance measures are of vital importance in designing any kind of distributed system, and that SMA can be useful in the design of the complicated mobile systems.     

HoneyCirculator: distributing credential honeytoken for introspection of web-based attack cycle

A web user who falsely accesses a compromised website is usually redirected to an adversary’s website and is forced to download malware after being exploited. Additionally, the adversary steals the user’s credentials by using information-leaking malware. The adversary may also try to compromise public websites owned by individual users by impersonating the website administrator using the stolen credentials. These compromised websites then become landing sites for drive-by download malware infection. Identifying malicious websites using crawling techniques requires a large amount of resources and time. To monitor the web-based attack cycle for effective detection and prevention, we propose a monitoring system called HoneyCirculator based on a honeytoken, which actively leaks bait credentials and lures adversaries to our decoy server that behaves like a compromised web content management system. To recursively analyze attack phases on the web-based attack cycle, our proposed system involves collecting malware, distributing bait credentials, monitoring fraudulent access, and inspecting compromised web content. It can instantly discover unknown malicious entities without conducting large-scale web crawling because of the direct monitoring behind the compromised web content management system. Our proposed system enables continuous and stable monitoring for about one year. In addition, almost all the malicious websites we discovered had not been previously registered in public blacklists.     

From Chemical Rules to Term Rewriting

In this paper, rule-based programming is explored in the field of automated generation of chemical reaction mechanisms. We explore a class of graphs and a graph rewriting relation where vertices are preserved and only edges are changed. We show how to represent cyclic labeled graphs by decorated labeled trees or forests, then how to transform trees into terms. A graph rewriting relation is defined, then simulated by a tree rewriting relation, which can be in turn simulated by a rewriting relation on equivalence classes of terms. As a consequence, this kind of graph rewriting can be implemented using term rewriting. This study is motivated by the design of the GasEl system for the generation of kinetics reactions mechanisms. In GasEl, chemical reactions correspond to graph rewrite rules and are implemented by conditional rewriting rules in ELAN. The control of their application is done through the ELAN strategy language.     

PVS#: Streamlined Tacticals for PVS

The semantics of a proof language relies on the representation of the state of a proof after a logical rule has been applied. This information, which is usually meaningless from a logical point of view, is fundamental to describe the control mechanism of the proof search provided by the language. In this paper, we present a monadic datatype to represent the state information of a proof and we illustrate its use in the PVS theorem prover. We show how this representation can be used to design a new set of powerful tacticals for PVS, called PVS#, that have a simpler and clearer semantics compared to the semantics of standard PVS tacticals.     

On the limits of refinement-testing for model-checking CSP

Refinement-checking, as embodied in tools like FDR, PAT and ProB, is a popular approach for model-checking refinement-closed predicates of CSP processes. We consider the limits of this approach to model-checking these kinds of predicates. By adopting Clarkson and Schneider’s hyperproperties framework, we show that every refinement-closed denotational predicate of finitely-nondeterministic, divergence-free CSP processes can be written as the conjunction of a safety predicate and the refinement-closure of a liveness predicate. We prove that every safety predicate is refinement-closed and that the safety predicates correspond precisely to the CSP refinement checks in finite linear observations models whose left-hand sides (i.e. specification processes) are independent of the systems to which they are applied. We then show that there exist important liveness predicates whose refinement-closures cannot be expressed as refinement checks in any finite linear observations model ${\mathcal{M}}$ , divergence-strict model ${\mathcal{M}^\Downarrow}$ or non-divergence-strict divergence-recording model ${\mathcal{M}^\#}$ , i.e. in any standard CSP model suitable for reasoning about the kinds of processes that FDR can handle, namely finitely-branching ones. These liveness predicates include liveness properties under intuitive fairness assumptions, branching-time liveness predicates and non-causation predicates for reasoning about authority. We conclude that alternative verification approaches, besides refinement-checking, currently under development for CSP should be further pursued.     

BSP-Why: A Tool for Deductive Verification of BSP Algorithms with Subgroup Synchronisation

We present bsp-why, a tool for deductive verification of bsp  algorithms with subgroup synchronisation. From bsp  programs, bsp-why generates sequential codes for the back-end condition generator why and thus benefits from its large range of existing provers. By enabling subgroups, the user can prove the correctness of programs that run on hierarchical machines—e.g. clusters of multi-cores. In general, bsp-why is able to generate proof obligations of mpi programs that only use collective operations. Our case studies are distributed state-space construction algorithms, the basis of model-checking.     

Prototype Platforms for Distributed Agreements

We present a prototype application for coordinating distributed agreements in multi-parties negotiations, where participants can dynamically join ongoing negotiations and where participants know only those parties they have interacted with. Our prototype is tailored to Ad-Hoc network scenarios involving the assignment of tasks for a rescue team operating over disaster areas. Our application is based on asynchronous communication and it exploits the d2pc protocol for committing or aborting a negotiation. Parties have been developed both in Jocaml+Perl and Polyphonic C. The implementation of the commit protocol allows components of both types to participate within the same negotiation.     

A short version of the visual aesthetics of websites inventory

The present paper addresses a need for a brief assessment instrument to measure perceived visual aesthetics of websites. A short version of the Visual Aesthetics of Websites inventory (VisAWI; Moshagen and Thielsch 2010 Moshagen, M., Thielsch, M. T., 2010. Facets of visual aesthetics. International Journal of Human-Computer Studies, 68, 689–709. doi: 10.1016/j.ijhcs.2010.05.006[Crossref], [Web of Science ®] , [Google Scholar]) called VisAWI-S was developed and evaluated in three studies comprising 1673 participants in total. The results indicate that the VisAWI-S is a reliable measure that captures a single dimension of perceived visual aesthetics and provides a good approximation to the full-length version. Convergent validity was established by a strong relationship to overall appeal. Evidence for divergent validity was obtained by weaker correlations to perceived usability, pragmatic quality and quality of content as well as by absence of a significant correlation to participants’ mood. In addition to this, the VisAWI-S was found to be substantially related to the intention to revisit a website. Overall, the results indicate that the VisAWI-S may gainfully be employed to measure perceived visual aesthetics of websites when assessment times must be kept to a minimum.     

A Simple Calculus for Proteins and Cells

The use of process calculi to represent biological systems has led to the design of different calculi such as brane calculi [Luca Cardelli. Brane calculi. In CMSB, pages 257–278, 2004] and κ-calculus [Vincent Danos and Cosimo Laneve. Formal molecular biology. Theoritical Computer Science, 325(1):69–110, 2004]. Both have proved to be useful to model different types of biological systems.As an attempt to unify the two directions, we introduce the bioκ-calculus, a simple calculus for describing proteins and cells, in which bonds are represented by means of shared names and interactions are modelled at the domain level. Protein-protein interactions have to be at most binary and cell interactions have to fit with sort constraints.We define the semantics of bioκ-calculus, analyse its properties, and discuss its expressiveness by modelling two significant examples: a signalling pathway and a virus infection.     

Aspect identification and ratings inference for hotel reviews

Today, a large volume of hotel reviews is available on many websites, such as TripAdvisor (http://www.tripadvisor.com) and Orbitz (http://www.orbitz.com). A typical review contains an overall rating, several aspect ratings, and review text. The rating is an abstract of review in terms of numerical points. The task of aspect-based opinion summarization is to extract aspect-specific opinions hidden in the reviews which do not have aspect ratings, so that users can quickly digest them without actually reading through them. The task consists of aspect identification and aspect rating inference. Most existing studies cannot utilize aspect ratings which become increasingly abundant on review hosts. In this paper, we propose two topic models which explicitly model aspect ratings as observed variables to improve the performance of aspect rating inference on unrated reviews. The experiment results show that our approaches outperform the existing methods on the data set crawled from TripAdvisor website.