Deterministic parsing of tree-structured data is usually performed sequentially left-to-right. Recently however, also motivated by the need to process extremely large data sets, a parallel version thereof has been devised which, thanks to the theoretical features of operator precedence languages (OPL) particularly well-suited to split the input into separate chunks, provided high improvements w.r.t. traditional sequential parsing. Further investigation pointed out a restriction imposed on the OPL formalism that prevents from fully exploiting parallelism and proposed an improvement of the original algorithm which proved effective in many practical cases. Stimulated by the above contribution here we remove the mentioned restriction on OPL and build a new parallel parser generator based thereon. We conducted a comparative experimentation among the three parallel algorithms that showed a consistent further improvement w.r.t. both the previous ones (with an exception in the case of purely sequential execution). Based on these early results, we believe that the horizon of parallel parsing large tree-structured data promises dramatic gains of efficiency in the analysis of this fundamental data structure.

Operator precedence languages (OPLs) enjoy the local parsability property, which means that a code fragment enclosed within a pair of markers playing the role of parentheses can be parsed with no knowledge of its external context. This property has been exploited to build parallel parsers for languages formalized as OPLs. It has been observed, however, that when the syntax trees of sentences have a linear substructure, parsing must necessarily proceed sequentially, making it ineffective to split such a subtree into chunks to be processed in parallel. This inconvenience derives from the hypothesis that the equality precedence relation cannot be cyclic, which has been so far assumed by most literature on OPLs. This hypothesis was motivated by the need to keep the mathematical notation as simple as possible, although it caused a discrepancy between the expressive power of operator precedence grammars and other formalisms defining OPLs such as operator precedence automata, monadic second order logic and operator precedence expressions, which do not assume acyclicity. We present an enriched version of operator precedence grammars, called cyclic , that allows for a simplified version of regular expressions in the right hand sides of grammar rules. For this class of operator precedence grammars the acyclicity hypothesis of the equality precedence relation is no more needed to guarantee the algebraic properties of the generated languages. The expressive power of the cyclic grammars is now fully equivalent to that of other formalisms defining OPLs. As a result, cyclic operator precedence grammars produce unranked syntax trees and sentences with flat unbounded substructures that can be naturally partitioned into chunks suitable for parallel parsing.

Abstract Operator Precedence Languages (OPL) have been recently identified as a suitable formalism for model checking recursive procedural programs, thanks to their ability of modeling the program stack. OPL requirements can be expressed in thePrecedence Oriented Temporal Logic(), which features modalities to reason on the natural matching between function calls and returns, exceptions, and other advanced programming constructs that previous approaches, such as Visibly Pushdown Languages, cannot model effectively. Existing approaches for model checking of have been designed following the explicit-state, automata-based approach, a feature that severely limits their scalability. In this paper, we give the first symbolic, SMT-based approach for model checking properties. While previous approaches construct the automaton for both the formula and the model of the program, we encode them into a (sequence of) SMT formulas. The search of a trace of the model witnessing a violation of the formula is then carried out by an SMT-solver, in a Bounded Model Checking fashion. We carried out an experimental evaluation, which shows the effectiveness of the proposed solution.

Additional Key Words and Phrases: Dependent types "Verified Functional Programming in Agda" is a practical introduction to verified functional programming, using the dependently typed functional programming language Agda.Agda is a programming language and proof-checker developed at Chalmers University by Ulf Norell; the version covered in the book is Agda 2. An important aspect to be noted is that the book is not based on Agda's standard library: The author developed an ad hoc library for the book, called IAL (Iowa Agda Library).The book under review is based on the 1.2 version of the library, freely available here: https://github.com/cedille/ialThe compelling idea of Agda is that, thanks to its very expressive and flexible type system, it can be used both as a programming language and as a proof-checker.Dependently typed languages offer types that can depend on values, so actual values can be used at the type level.In a nutshell, the idea of verified functional programming is to exploit the Curry-Howard isomorphism between proofs and programs to write functions that verify the properties encoded in their types.The Curry-Howard isomorphism is basically a correspondence between Intuitionistic (or Constructive) Logic and Typed Lambda Calculus, so proofs correspond to code and logic formulae to types: To give the reader an intuitive idea, conjunction corresponds to product types, disjunction to sum types, implication to function types, existential quantification to dependent pair types (where the type of the second component depends on the value of the first component), and universal quantification to dependent function types (where the return type depends on the value of the input value).A typical example of a dependent type is that of vectors encoding the value of their length together with the vector content: In this kind of setting, it is possible, for instance, to state in the signature of the append function the property that the length of the resulting vector is the sum of the lengths of the input vectors.This approach can be used in general to define very expressive types, and then to use them in the signature of functions to state some of their properties.This is called in the book internal verification, because the property is expressed directly in the type of the function, while its proof is in its code: If the code is correct for the type checker, then the property is proved.Agda can be also used as a proof-checker: We can define a function where the signature is in fact a statement (e.g., a complex property of other functions), and its implementation is its actual proof-this is called in the book external verification.

A classic result in formal language theory is the equivalence among non-counting, or aperiodic, regular languages, and languages defined through star-free regular expressions, or first-order logic. Past attempts to extend this result beyond the realm of regular languages have met with difficulties: for instance it is known that star-free tree languages may violate the non-counting property and there are aperiodic tree languages that cannot be defined through first-order logic. We extend such classic equivalence results to a significant family of deterministic context-free languages, the operator-precedence languages (OPL), which strictly includes the widely investigated visibly pushdown, alias input-driven, family and other structured context-free languages. The OP model originated in the '60s for defining programming languages and is still used by high performance compilers; its rich algebraic properties have been investigated initially in connection with grammar learning and recently completed with further closure properties and with monadic second order logic definition. We introduce an extension of regular expressions, the OP-expressions (OPE) which define the OPLs and, under the star-free hypothesis, define first-order definable and non-counting OPLs. Then, we prove, through a fairly articulated grammar transformation, that aperiodic OPLs are first-order definable. Thus, the classic equivalence of star-freeness, aperiodicity, and first-order definability is established for the large and powerful class of OPLs. We argue that the same approach can be exploited to obtain analogous results for visibly pushdown languages too.

The problem of extending model checking from finite state machines to procedural programs has fostered much research toward the definition of temporal logics for reasoning on context-free structures. The most notable of such results are temporal logics on Nested Words, such as CaRet and NWTL. Recently, Precedence Oriented Temporal Logic (POTL) has been introduced to specify and prove properties of programs coded trough an Operator Precedence Language (OPL). POTL is complete w.r.t. the FO restriction of the MSO logic previously defined as a logic fully equivalent to OPL. POTL increases NWTL’s expressive power in a perfectly parallel way as OPLs are more powerful that nested words. In this article, we produce a model checker, named POMC, for OPL programs to prove properties expressed in POTL. To the best of our knowledge, POMC is the first implemented and openly available model checker for proving tree-structured properties of recursive procedural programs. We also report on the experimental evaluation we performed on POMC on a nontrivial benchmark.

The problem of model checking procedural programs has fostered much research towards the definition of temporal logics for reasoning on context-free structures. The most notable of such results are temporal logics on Nested Words, such as CaRet and NWTL. Recently, the logic OPTL was introduced, based on the class of Operator Precedence Languages (OPLs), more powerful than Nested Words. We define the new OPL-based logic POTL and prove its FO-completeness. POTL improves on NWTL by enabling the formulation of requirements involving pre/post-conditions, stack inspection, and others in the presence of exception-like constructs. It improves on OPTL too, which instead we show not to be FO-complete; it also allows to express more easily stack inspection and function-local properties. In a companion paper we report a model checking procedure for POTL and experimental results based on a prototype tool developed therefor. For completeness a short summary of this complementary result is provided in this paper too.

Abstract The problem of model checking procedural programs has fostered much research towards the definition of temporal logics for reasoning on context-free structures. The most notable of such results are temporal logics on Nested Words, such as CaRet and NWTL. Recently, the logic OPTL was introduced, based on the class of Operator Precedence Languages (OPL), more powerful than Nested Words. We define the new OPL-based logic POTL, and provide a model checking procedure for it. POTL improves on NWTL by enabling the formulation of requirements involving pre/post-conditions, stack inspection, and others in the presence of exception-like constructs. It improves on OPTL by being FO-complete, and by expressing more easily stack inspection and function-local properties. We developed a model checking tool for POTL, which we experimentally evaluate on some interesting use-cases.

In the last years renewed investigation of operator precedence languages (OPL) led to discover important properties thereof: OPL are closed with respect to all major operations, are characterized, besides the original grammar family, in terms of an automata family (OPA) and an MSO logic; furthermore they significantly generalize the well-known visibly pushdown languages (VPL). In another area of research, quantitative models of systems are also greatly in demand. In this paper, we lay the foundation to marry these two research fields. We introduce weighted operator precedence automata and show how they are both strict extensions of OPA and weighted visibly pushdown automata. We prove a Nivat-like result which shows that quantitative OPL can be described by unweighted OPA and very particular weighted OPA. In a Büchi-like theorem, we show that weighted OPA are expressively equivalent to a weighted MSO-logic for OPL.

Operator precedence languages were introduced half a century ago by Robert Floyd to support deterministic and efficient parsing of context-free languages. Recently, we renewed our interest in this class of languages thanks to a few distinguishing properties that make them attractive for exploiting various modern technologies. Precisely, their local parsability enables parallel and incremental parsing, whereas their closure properties make them amenable to automatic verification techniques, including model checking. In this paper we provide a fairly complete theory of this class of languages: we introduce a class of automata with the same recognizing power as the generative power of their grammars; we provide a characterization of their sentences in terms of monadic second-order logic as has been done in previous literature for more restricted language classes such as regular, parenthesis, and input-driven ones; we investigate preserved and lost properties when extending the language sentences from finite length to infinite length ($\omega$-languages). As a result, we obtain a class of languages that enjoys many of the nice properties of regular languages (closure and decidability properties, logic characterization) but is considerably larger than other families---typically parenthesis and input-driven ones---with the same properties, covering “almost” all deterministic languages.

Self-adaptive software has become increasingly important to address the new challenges of complex computing systems. To achieve adaptation, software must be designed and implemented by following suitable criteria, methods, and strategies. Past research has been mostly addressing adaptation by developing solutions at the software architecture level. This work, instead, focuses on finer-grain programming language-level solutions. We analyze three main linguistic approaches: metaprogramming, aspect-oriented programming, and context-oriented programming. The first two are general-purpose linguistic mechanisms, whereas the third is a specific and focused approach developed to support context-aware applications. This paradigm provides specialized language-level abstractions to implement dynamic adaptation and modularize behavioral variations in adaptive systems. The article shows how the three approaches can support the implementation of adaptive systems and compares the pros and cons offered by each solution.

We introduce bounded satisfiability checking, a verification technique that extends bounded model checking by allowing also the analysis of a descriptive model , consisting of temporal logic formulae, instead of the more customary operational model , consisting of a state transition system. We define techniques for encoding temporal logic formulae into Boolean logic that support the use of bi-infinite time domain and of metric time operators. In the framework of bounded satisfiability checking, we show how a descriptive model can be refined into an operational one, and how the correctness of such a refinement can be verified for the bounded case, setting the stage for a stepwise system development method based on a bounded model refinement. Finally, we show how the adoption of a modular approach can make the bounded refinement process more manageable and efficient. All introduced concepts are extensively applied to a set of case studies, and thoroughly experimented through Zot, our SAT solver-based verification toolset.

This paper presents a novel approach to the design of self-adaptive service-oriented applications based on a new model called service tiles. The approach allows designers to develop a service-oriented system by building an assembly of component services that accomplishes the given goal. The assembly is computed automatically starting from the specification of a subset of the whole system, a few constraints, and the goals the application should fulfill. An application designed according to the service-tile model can also dynamically self-adapt by replacing, in part or entirely, services in the assembly whenever they fail or the application context changes. The service-tile design technique has been implemented in a prototype and some experiments with several examples demonstrate the feasibility of the approach and its practical efficiency.

An important problem that arises during the execution of service-based applications concerns the ability to determine whether a running service can be substituted with one with a different interface, for example if the former is no longer available. Standard Bounded Model Checking techniques can be used to perform this check, but they must be able to provide answers very quickly, to avoid that the check may affect the operativeness of the application, instead of aiding it. The problem becomes even more complex when conversational services are considered, i.e., services that expose operations that have Input/Output data dependencies among them. In this paper we introduce a formal verification technique for an extension of Linear Temporal Logic that allows users to include in formulae constraints on integer variables. This technique applied to the substitutability problem for conversational services is shown to be considerably faster and with smaller memory footprint than existing ones.

This paper defines CLTLB(D), an extension of PLTLB (PLTL with both past and future operators) augmented with atomic formulae built over a constraint system D. The paper introduces suitable restrictions and assumptions that make the satisfiability problem decidable in many cases, although the problem is undecidable in the general case. Decidability is shown for a large class of constraint systems, and an encoding into Boolean logic is defined. This paves the way for applying existing SMT-solvers for checking the Bounded Reachability problem, as shown by various experimental results.

A core problem in formal methods is the transition from informal requirements to formal specifications. Especially when specifying reactive systems, many formalisms require the user to either understand a complex mathematical theory and notation or to derive details not given in the requirements, such as the state space of the problem. While formalizing a real-world requirements document, we developed a technique where not states but signal patterns are the main elements. We argue that it supports a formalization that is often closer to the informal requirements and thus provides a smoother transition to formal methods. As only tables of regular expressions are used for notation, the technique can easily be understood by non-mathematicians. Many properties, such as consistency, can be checked automatically on these specifications. Besides the formal foundation of our approach, this paper presents prototypical tool support and first results from an industrial case study.

In bounded model checking (BMC) a system is modeled with a finite automaton and various desired properties with temporal logic formulae. Property verification is achieved by translation into boolean logic and the application of SAT-solvers. bounded satisfiability checking (BSC) adopts a similar approach, but both the system and the properties are modeled with temporal logic formulae, without an underlying operational model. Hence, BSC supports a higher-level, descriptive approach to system specification and analysis. We compare the performance of BMC and BSC over a set of case studies, using the Zot tool to translate automata and temporal logic formulae into boolean logic. We also propose a method to check whether an operational model is a correct implementation (refinement) of a temporal logic model, and assess its effectiveness on the same set of case studies. Our experimental results show the feasibility of BSC and refinement checking, with modest performance loss w.r.t. BMC.

Model checking techniques have traditionally dealt with temporal logic languages and automata interpreted over ω-words, i.e., infinite in the future but finite in the past. However, time with also an infinite past is a useful abstraction in specification. It allows one to ignore the complexity of system initialization in much the same way as system termination may be abstracted away by allowing an infinite future. One can then write specifications that are simpler and more easily understandable, because they do not include the description of the operations (such as configuration or installation) typically performed at system deployment time. The present paper is centered on the problem of satisfiability checking of linear temporal logic (LTL) formulae with past operators. We show that bounded model checking techniques can be adapted to deal with bi-infinite time in temporal logic, without incurring in any performance loss. Our claims are supported by a tool, whose application to a case study shows that satisfiability checking may be feasible also on nontrivial examples of temporal logic specifications.

The paper "An Interval Logic for Real-Time System Specification" (Mattolini and Nesi, IEEE Trans. Software Eng., vol. 27, no. 3, pp. 208-227, Mar. 2001) presents the TILCO specification language and compares it to other existing similar languages. In this comment, we show that several of the logic formulas used for the comparison are flawed and/or overly complicated and we explain why, in this respect, the comparison is moot

The design of distributed applications in a CORBA-based environment can be carried out by means of an incremental approach, which starts from the specification and leads to the high-level architectural design. This article discusses a methodology to transform a formal specification written in TRIO into a high-level design document written in an extension of TRIO, named TRIO/CORBA (TC). The TC language is suited to formally describe the high-level architecture of a CORBA-based application. As a result, designers are offered high-level concepts that precisely define the architectural elements of an application. Furthermore, TC offers mechanisms to extend its base semantics, and can be adapted to future developments and enhancements in the CORBA standard. The methodology and the associated language are presented through a case study derived from a real Supervision and Control System.

The present paper reports the experience of a joint project between Politecnico di Milano and Italian State Railway FS, Infrastructure Department (became Rete Ferroviaria Italiana SpA: RFI SpA). The purpose of the project was to define procedures and rules for managing software procurement for safety-critical signalling equipment. The project covers all phases of system development, from requirements elicitation to implementation and final validation, providing requirements on methods, languages and tools to be used during software development, without any bias towards any particular technology or tool provider. The results are consistent with, and acceptable against, international standards. In particular, requirements/recommendations have been issued, tailored on various kinds of systems under examination, concerning: a) methods, techniques, languages and tools; b) organization of the provider company in terms of independence and responsibility of participating actors; c) documentation to be produced by the provider. An experimental evaluation of formal specification methods applied to signalling systems is also reported.

The design of distributed applications in a CORBA based environment can be carried out by means of an incremental approach, which starts from the specification and leads to the high level architectural design. This is done by introducing in the specification all typical elements of CORBA and by providing a methodological support to the designers. The paper discusses a methodology to transform a formal specification written in TRIO into a high level design document written using an extension of TRIO named TC. The TC language is suited to formally describe the high level architecture of a CORBA based application. The methodology and the associated language are presented by means of an example involving a real Supervision and Control System.