-
SMT-based Symbolic Model-Checking for Operator Precedence Languages
Authors:
Michele Chiari,
Luca Geatti,
Nicola Gigante,
Matteo Pradella
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 the Precedence Oriented Temporal Logic (POTL), which features modalities to reason on the natural matching between function calls and returns, exceptions, and other adv…
▽ More
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 the Precedence Oriented Temporal Logic (POTL), 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 POTL 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 POTL properties. While previous approaches construct the automaton for both the POTL 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.
△ Less
Submitted 18 May, 2024;
originally announced May 2024.
-
Cyclic Operator Precedence Grammars for Parallel Parsing
Authors:
Michele Chiari,
Dino Mandrioli,
Matteo Pradella
Abstract:
Operator precedence languages (OPL) enjoy the local parsability property, which essentially means that a code fragment enclosed within a pair of markers -- playing the role of parentheses -- can be compiled with no knowledge of its external context. Such a property has been exploited to build parallel compilers for languages formalized as OPLs. It has been observed, however, that when the syntax t…
▽ More
Operator precedence languages (OPL) enjoy the local parsability property, which essentially means that a code fragment enclosed within a pair of markers -- playing the role of parentheses -- can be compiled with no knowledge of its external context. Such a property has been exploited to build parallel compilers for languages formalized as OPLs. It has been observed, however, that when the syntax trees of the sentences have a linear substructure, its parsing must necessarily proceed sequentially making it impossible to split such a subtree into chunks to be processed in parallel. Such an inconvenience is due to the fact that so far much literature on OPLs has assumed the hypothesis that equality precedence relation cannot be cyclic. This hypothesis was motivated by the need to keep the mathematical notation as simple as possible.
We present an enriched version of operator precedence grammars, called cyclic, that allows to use a simplified version of regular expressions in the right hand sides of grammar's 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 such as operator precedence automata, monadic second order logic and operator precedence expressions. As a result cyclic operator precedence grammars now produce also unranked syntax trees and sentences with flat unbounded substructures that can be naturally partitioned into chunks suitable for parallel parsing.
△ Less
Submitted 8 September, 2023;
originally announced September 2023.
-
Lecture Notes on Monadic First- and Second-Order Logic on Strings
Authors:
Dino Mandrioli,
Davide Martinenghi,
Angelo Morzenti,
Matteo Pradella,
Matteo Rossi
Abstract:
These notes present the essentials of first- and second-order monadic logics on strings with introductory purposes. We discuss Monadic First-Order logic and show that it is strictly less expressive than Finite-State Automata, in that it only captures a strict subset of Regular Languages -- the non-counting ones. We then introduce Monadic Second-Order logic; such a logic is, syntactically, a supers…
▽ More
These notes present the essentials of first- and second-order monadic logics on strings with introductory purposes. We discuss Monadic First-Order logic and show that it is strictly less expressive than Finite-State Automata, in that it only captures a strict subset of Regular Languages -- the non-counting ones. We then introduce Monadic Second-Order logic; such a logic is, syntactically, a superset of Monadic First-Order logic and captures Regular Languages exactly. We also show how to transform an automaton into a corresponding formula and vice versa. Finally, we discuss the use of logical characterizations of classes of languages as the basis for automatic verification techniques.
△ Less
Submitted 25 January, 2023;
originally announced January 2023.
-
TotalSegmentator: robust segmentation of 104 anatomical structures in CT images
Authors:
Jakob Wasserthal,
Hanns-Christian Breit,
Manfred T. Meyer,
Maurice Pradella,
Daniel Hinck,
Alexander W. Sauter,
Tobias Heye,
Daniel Boll,
Joshy Cyriac,
Shan Yang,
Michael Bach,
Martin Segeroth
Abstract:
We present a deep learning segmentation model that can automatically and robustly segment all major anatomical structures in body CT images. In this retrospective study, 1204 CT examinations (from the years 2012, 2016, and 2020) were used to segment 104 anatomical structures (27 organs, 59 bones, 10 muscles, 8 vessels) relevant for use cases such as organ volumetry, disease characterization, and s…
▽ More
We present a deep learning segmentation model that can automatically and robustly segment all major anatomical structures in body CT images. In this retrospective study, 1204 CT examinations (from the years 2012, 2016, and 2020) were used to segment 104 anatomical structures (27 organs, 59 bones, 10 muscles, 8 vessels) relevant for use cases such as organ volumetry, disease characterization, and surgical or radiotherapy planning. The CT images were randomly sampled from routine clinical studies and thus represent a real-world dataset (different ages, pathologies, scanners, body parts, sequences, and sites). The authors trained an nnU-Net segmentation algorithm on this dataset and calculated Dice similarity coefficients (Dice) to evaluate the model's performance. The trained algorithm was applied to a second dataset of 4004 whole-body CT examinations to investigate age dependent volume and attenuation changes. The proposed model showed a high Dice score (0.943) on the test set, which included a wide range of clinical data with major pathologies. The model significantly outperformed another publicly available segmentation model on a separate dataset (Dice score, 0.932 versus 0.871, respectively). The aging study demonstrated significant correlations between age and volume and mean attenuation for a variety of organ groups (e.g., age and aortic volume; age and mean attenuation of the autochthonous dorsal musculature). The developed model enables robust and accurate segmentation of 104 anatomical structures. The annotated dataset (https://doi.org/10.5281/zenodo.6802613) and toolkit (https://www.github.com/wasserth/TotalSegmentator) are publicly available.
△ Less
Submitted 16 June, 2023; v1 submitted 11 August, 2022;
originally announced August 2022.
-
Static Analysis of Infrastructure as Code: a Survey
Authors:
Michele Chiari,
Michele De Pascalis,
Matteo Pradella
Abstract:
The increasing use of Infrastructure as Code (IaC) in DevOps leads to benefits in speed and reliability of deployment operation, but extends to infrastructure challenges typical of software systems. IaC scripts can contain defects that result in security and reliability issues in the deployed infrastructure: techniques for detecting and preventing them are needed. We analyze and survey the current…
▽ More
The increasing use of Infrastructure as Code (IaC) in DevOps leads to benefits in speed and reliability of deployment operation, but extends to infrastructure challenges typical of software systems. IaC scripts can contain defects that result in security and reliability issues in the deployed infrastructure: techniques for detecting and preventing them are needed. We analyze and survey the current state of research in this respect by conducting a literature review on static analysis techniques for IaC. We describe analysis techniques, defect categories and platforms targeted by tools in the literature.
△ Less
Submitted 21 June, 2022;
originally announced June 2022.
-
Diversity patterns and speciation processes in a two-island system with continuous migration
Authors:
Débora Princepe,
Simone Czarnobai,
Thiago M. Pradella,
Rodrigo A. Caetano,
Flavia M. D. Marquitti,
Marcus A. M. de Aguiar,
Sabrina B. L. Araujo
Abstract:
Geographic isolation is a central mechanism of speciation, but perfect isolation of populations is rare. Although speciation can be hindered if gene flow is large, intermediate levels of migration can enhance speciation by introducing genetic novelty in the semi-isolated populations or founding small communities of migrants. Here we consider a two island neutral model of speciation with continuous…
▽ More
Geographic isolation is a central mechanism of speciation, but perfect isolation of populations is rare. Although speciation can be hindered if gene flow is large, intermediate levels of migration can enhance speciation by introducing genetic novelty in the semi-isolated populations or founding small communities of migrants. Here we consider a two island neutral model of speciation with continuous migration and study diversity patterns as a function of the migration probability, population size, and number of genes involved in reproductive isolation (dubbed as genome size). For small genomes, low levels of migration induce speciation on the islands that otherwise would not occur. Diversity, however, drops sharply to a single species inhabiting both islands as the migration probability increases. For large genomes, sympatric speciation occurs even when the islands are strictly isolated. Then species richness per island increases with the probability of migration, but the total number of species decreases as they become cosmopolitan. For each genome size, there is an optimal migration intensity for each population size that maximizes the number of species. We discuss the observed modes of speciation induced by migration and how they increase species richness in the insular system while promoting asymmetry between the islands and hindering endemism.
△ Less
Submitted 7 June, 2022; v1 submitted 23 February, 2022;
originally announced February 2022.
-
A First-Order Complete Temporal Logic for Structured Context-Free Languages
Authors:
Michele Chiari,
Dino Mandrioli,
Matteo Pradella
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 (OPLs), more powerful than Nested Words. We define t…
▽ More
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.
△ Less
Submitted 28 July, 2022; v1 submitted 22 May, 2021;
originally announced May 2021.
-
Aperiodicity, Star-freeness, and First-order Logic Definability of Operator Precedence Languages
Authors:
Dino Mandrioli,
Matteo Pradella,
Stefano Crespi Reghizzi
Abstract:
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 the…
▽ More
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.
△ Less
Submitted 21 November, 2023; v1 submitted 1 June, 2020;
originally announced June 2020.
-
POTL: A First-Order Complete Temporal Logic for Operator Precedence Languages
Authors:
Michele Chiari,
Dino Mandrioli,
Matteo Pradella
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 th…
▽ More
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, prove its FO-completeness, 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.
△ Less
Submitted 31 October, 2020; v1 submitted 21 October, 2019;
originally announced October 2019.
-
Temporal Logic and Model Checking for Operator Precedence Languages
Authors:
Michele Chiari,
Dino Mandrioli,
Matteo Pradella
Abstract:
In the last decades much research effort has been devoted to extending the success of model checking from the traditional field of finite state machines and various versions of temporal logics to suitable subclasses of context-free languages and appropriate extensions of temporal logics. To the best of our knowledge such attempts only covered structured languages, i.e. languages whose structure is…
▽ More
In the last decades much research effort has been devoted to extending the success of model checking from the traditional field of finite state machines and various versions of temporal logics to suitable subclasses of context-free languages and appropriate extensions of temporal logics. To the best of our knowledge such attempts only covered structured languages, i.e. languages whose structure is immediately "visible" in their sentences, such as tree-languages or visibly pushdown ones. In this paper we present a new temporal logic suitable to express and automatically verify properties of operator precedence languages. This "historical" language family has been recently proved to enjoy fundamental algebraic and logic properties that make it suitable for model checking applications yet breaking the barrier of visible-structure languages (in fact the original motivation of its inventor Floyd was just to support efficient parsing, i.e. building the "hidden syntax tree" of language sentences). We prove that our logic is at least as expressive as analogous logics defined for visible pushdown languages yet covering a much more powerful family; we design a procedure that, given a formula in our logic builds an automaton recognizing the sentences satisfying the formula, whose size is at most exponential in the length of the formula.
△ Less
Submitted 9 September, 2018;
originally announced September 2018.
-
Higher-Order Operator Precedence Languages
Authors:
Stefano Crespi Reghizzi,
Matteo Pradella
Abstract:
Floyd's Operator Precedence (OP) languages are a deterministic context-free family having many desirable properties. They are locally and parallely parsable, and languages having a compatible structure are closed under Boolean operations, concatenation and star; they properly include the family of Visibly Pushdown (or Input Driven) languages. OP languages are based on three relations between any t…
▽ More
Floyd's Operator Precedence (OP) languages are a deterministic context-free family having many desirable properties. They are locally and parallely parsable, and languages having a compatible structure are closed under Boolean operations, concatenation and star; they properly include the family of Visibly Pushdown (or Input Driven) languages. OP languages are based on three relations between any two consecutive terminal symbols, which assign syntax structure to words. We extend such relations to k-tuples of consecutive terminal symbols, by using the model of strictly locally testable regular languages of order k at least 3. The new corresponding class of Higher-order Operator Precedence languages (HOP) properly includes the OP languages, and it is still included in the deterministic (also in reverse) context free family. We prove Boolean closure for each subfamily of structurally compatible HOP languages. In each subfamily, the top language is called max-language. We show that such languages are defined by a simple cancellation rule and we prove several properties, in particular that max-languages make an infinite hierarchy ordered by parameter k. HOP languages are a candidate for replacing OP languages in the various applications where they have have been successful though sometimes too restrictive.
△ Less
Submitted 21 August, 2017; v1 submitted 25 May, 2017;
originally announced May 2017.
-
Generalizing input-driven languages: theoretical and practical benefits
Authors:
Dino Mandrioli,
Matteo Pradella
Abstract:
Regular languages (RL) are the simplest family in Chomsky's hierarchy. Thanks to their simplicity they enjoy various nice algebraic and logic properties that have been successfully exploited in many application fields. Practically all of their related problems are decidable, so that they support automatic verification algorithms. Also, they can be recognized in real-time.
Context-free languages…
▽ More
Regular languages (RL) are the simplest family in Chomsky's hierarchy. Thanks to their simplicity they enjoy various nice algebraic and logic properties that have been successfully exploited in many application fields. Practically all of their related problems are decidable, so that they support automatic verification algorithms. Also, they can be recognized in real-time.
Context-free languages (CFL) are another major family well-suited to formalize programming, natural, and many other classes of languages; their increased generative power w.r.t. RL, however, causes the loss of several closure properties and of the decidability of important problems; furthermore they need complex parsing algorithms. Thus, various subclasses thereof have been defined with different goals, spanning from efficient, deterministic parsing to closure properties, logic characterization and automatic verification techniques.
Among CFL subclasses, so-called structured ones, i.e., those where the typical tree-structure is visible in the sentences, exhibit many of the algebraic and logic properties of RL, whereas deterministic CFL have been thoroughly exploited in compiler construction and other application fields.
After surveying and comparing the main properties of those various language families, we go back to operator precedence languages (OPL), an old family through which R. Floyd pioneered deterministic parsing, and we show that they offer unexpected properties in two fields so far investigated in totally independent ways: they enable parsing parallelization in a more effective way than traditional sequential parsers, and exhibit the same algebraic and logic properties so far obtained only for less expressive language families.
△ Less
Submitted 2 May, 2017;
originally announced May 2017.
-
Weighted Operator Precedence Languages
Authors:
Manfred Droste,
Stefan Dück,
Dino Mandrioli,
Matteo Pradella
Abstract:
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 and an MSO logic; furthermore they significantly generalize the well-known visibly pushdown languages (VPL). In another area of researc…
▽ More
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 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.
△ Less
Submitted 15 February, 2017;
originally announced February 2017.
-
Operator Precedence ω-languages
Authors:
Federica Panella,
Matteo Pradella,
Dino Mandrioli,
Violetta Lonati
Abstract:
ω-languages are becoming more and more relevant nowadays when most applications are 'ever-running'. Recent literature, mainly under the motivation of widening the application of model checking techniques, extended the analysis of these languages from the simple regular ones to various classes of languages with 'visible syntax structure', such as visibly pushdown languages (VPLs). Operator preceden…
▽ More
ω-languages are becoming more and more relevant nowadays when most applications are 'ever-running'. Recent literature, mainly under the motivation of widening the application of model checking techniques, extended the analysis of these languages from the simple regular ones to various classes of languages with 'visible syntax structure', such as visibly pushdown languages (VPLs). Operator precedence languages (OPLs), instead, were originally defined to support deterministic parsing and, though seemingly unrelated, exhibit interesting relations with these classes of languages: OPLs strictly include VPLs, enjoy all relevant closure properties and have been characterized by a suitable automata family and a logic notation. In this paper we introduce operator precedence ω-languages (ωOPLs), investigating various acceptance criteria and their closure properties. Whereas some properties are natural extensions of those holding for regular languages, others required novel investigation techniques. Application-oriented examples show the gain in expressiveness and verifiability offered by ωOPLs w.r.t. smaller classes.
△ Less
Submitted 2 July, 2013; v1 submitted 11 January, 2013;
originally announced January 2013.
-
Constraint LTL Satisfiability Checking without Automata
Authors:
Marcello M. Bersani,
Achille Frigeri,
Angelo Morzenti,
Matteo Pradella,
Matteo Rossi,
Pierluigi San Pietro
Abstract:
This paper introduces a novel technique to decide the satisfiability of formulae written in the language of Linear Temporal Logic with Both future and past operators and atomic formulae belonging to constraint system D (CLTLB(D) for short). The technique is based on the concept of bounded satisfiability, and hinges on an encoding of CLTLB(D) formulae into QF-EUD, the theory of quantifier-free equa…
▽ More
This paper introduces a novel technique to decide the satisfiability of formulae written in the language of Linear Temporal Logic with Both future and past operators and atomic formulae belonging to constraint system D (CLTLB(D) for short). The technique is based on the concept of bounded satisfiability, and hinges on an encoding of CLTLB(D) formulae into QF-EUD, the theory of quantifier-free equality and uninterpreted functions combined with D. Similarly to standard LTL, where bounded model-checking and SAT-solvers can be used as an alternative to automata-theoretic approaches to model-checking, our approach allows users to solve the satisfiability problem for CLTLB(D) formulae through SMT-solving techniques, rather than by checking the emptiness of the language of a suitable automaton A_φ. The technique is effective, and it has been implemented in our Zot formal verification tool.
△ Less
Submitted 11 February, 2014; v1 submitted 4 May, 2012;
originally announced May 2012.
-
Logic Characterization of Floyd Languages
Authors:
Violetta Lonati,
Dino Mandrioli,
Matteo Pradella
Abstract:
Floyd languages (FL), alias Operator Precedence Languages, have recently received renewed attention thanks to their closure properties and local parsability which allow one to apply automatic verification techniques (e.g. model checking) and parallel and incremental parsing. They properly include various other classes, noticeably Visual Pushdown languages. In this paper we provide a characterizati…
▽ More
Floyd languages (FL), alias Operator Precedence Languages, have recently received renewed attention thanks to their closure properties and local parsability which allow one to apply automatic verification techniques (e.g. model checking) and parallel and incremental parsing. They properly include various other classes, noticeably Visual Pushdown languages. In this paper we provide a characterization of FL in terms a monadic second order logic (MSO), in the same style as Buchi's one for regular languages. We prove the equivalence between automata recognizing FL and the MSO formalization.
△ Less
Submitted 20 April, 2012;
originally announced April 2012.
-
Context-Oriented Programming: A Programming Paradigm for Autonomic Systems
Authors:
Guido Salvaneschi,
Carlo Ghezzi,
Matteo Pradella
Abstract:
Dynamic software adaptability is one of the central features leveraged by autonomic computing. However, developing software that changes its behavior at run time adapting to the operational conditions is a challenging task. Several approaches have been proposed in the literature to attack this problem at different and complementary abstraction levels: software architecture, middleware, and program…
▽ More
Dynamic software adaptability is one of the central features leveraged by autonomic computing. However, developing software that changes its behavior at run time adapting to the operational conditions is a challenging task. Several approaches have been proposed in the literature to attack this problem at different and complementary abstraction levels: software architecture, middleware, and programming level. We focus on the support that ad-hoc programming language constructs may provide to support dynamically adaptive behaviors. We introduce context-oriented programming languages and we present a framework that positions the supported paradigm in the MAPE-K autonomic loop. We discuss the advantages of using context-oriented programming languages instead of other mainstream approaches based on dynamic aspect oriented programming languages and present a case study that shows how the proposed programming style naturally fits dynamic adaptation requirements. Finally, we discuss some known problems and outline a number of open research challenges.
△ Less
Submitted 30 March, 2012; v1 submitted 30 April, 2011;
originally announced May 2011.
-
JavaCtx: Seamless Toolchain Integration for Context-Oriented Programming
Authors:
Guido Salvaneschi,
Carlo Ghezzi,
Matteo Pradella
Abstract:
Context-oriented programming is an emerging paradigm addressing at the language level the issue of dynamic software adaptation and modularization of context-specific concerns. In this paper we propose JavaCtx, a tool which employs coding conventions to generate the context-aware semantics for Java programs and subsequently weave it into the application. The contribution of JavaCtx is twofold: the…
▽ More
Context-oriented programming is an emerging paradigm addressing at the language level the issue of dynamic software adaptation and modularization of context-specific concerns. In this paper we propose JavaCtx, a tool which employs coding conventions to generate the context-aware semantics for Java programs and subsequently weave it into the application. The contribution of JavaCtx is twofold: the design of a set of coding conventions which allow to write context-oriented software in plain Java and the concept of context-oriented semantics injection, which allows to introduce the context-aware semantics without a source-to-source compilations process which disrupts the structure of the code. Both these points allow to seamless integrate JavaCtx in the existing industrial-strength appliances and by far ease the development of context-oriented software.
△ Less
Submitted 7 April, 2011;
originally announced April 2011.
-
Precedence Automata and Languages
Authors:
Violetta Lonati,
Dino Mandrioli,
Matteo Pradella
Abstract:
Operator precedence grammars define a classical Boolean and deterministic context-free family (called Floyd languages or FLs). FLs have been shown to strictly include the well-known visibly pushdown languages, and enjoy the same nice closure properties. We introduce here Floyd automata, an equivalent operational formalism for defining FLs. This also permits to extend the class to deal with infinit…
▽ More
Operator precedence grammars define a classical Boolean and deterministic context-free family (called Floyd languages or FLs). FLs have been shown to strictly include the well-known visibly pushdown languages, and enjoy the same nice closure properties. We introduce here Floyd automata, an equivalent operational formalism for defining FLs. This also permits to extend the class to deal with infinite strings to perform for instance model checking.
△ Less
Submitted 30 November, 2011; v1 submitted 10 December, 2010;
originally announced December 2010.
-
SMT-based Verification of LTL Specifications with Integer Constraints and its Application to Runtime Checking of Service Substitutability
Authors:
Marcello M. Bersani,
Luca Cavallaro,
Achille Frigeri,
Matteo Pradella,
Matteo Rossi
Abstract:
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, lest the check ha…
▽ More
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, lest the check hampers 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.
△ Less
Submitted 16 April, 2010;
originally announced April 2010.
-
Bounded Reachability for Temporal Logic over Constraint Systems
Authors:
Marcello M. Bersani,
Achille Frigeri,
Angelo Morzenti,
Matteo Pradella,
Matteo Rossi,
Pierluigi San Pietro
Abstract:
We present CLTLB(D), an extension of PLTLB (PLTL with both past and future operators) augmented with atomic formulae built over a constraint system D. Even for decidable constraint systems, satisfiability and Model Checking problem of such logic can be undecidable. We introduce suitable restrictions and assumptions that are shown to make the satisfiability problem for the extended logic decidable.…
▽ More
We present CLTLB(D), an extension of PLTLB (PLTL with both past and future operators) augmented with atomic formulae built over a constraint system D. Even for decidable constraint systems, satisfiability and Model Checking problem of such logic can be undecidable. We introduce suitable restrictions and assumptions that are shown to make the satisfiability problem for the extended logic decidable. Moreover for a large class of constraint systems we propose an encoding that realize an effective decision procedure for the Bounded Reachability problem.
△ Less
Submitted 20 April, 2010; v1 submitted 7 April, 2010;
originally announced April 2010.
-
A User's Guide to Zot
Authors:
Matteo Pradella
Abstract:
Zot is an agile and easily extendible bounded model checker, which can be downloaded at http://home.dei.polimi.it/pradella/. The tool supports different logic languages through a multi-layered approach: its core uses PLTL, and on top of it a decidable predicative fragment of TRIO is defined. An interesting feature of Zot is its ability to support different encodings of temporal logic as SAT prob…
▽ More
Zot is an agile and easily extendible bounded model checker, which can be downloaded at http://home.dei.polimi.it/pradella/. The tool supports different logic languages through a multi-layered approach: its core uses PLTL, and on top of it a decidable predicative fragment of TRIO is defined. An interesting feature of Zot is its ability to support different encodings of temporal logic as SAT problems by means of plug-ins. This approach encourages experimentation, as plug-ins are expected to be quite simple, compact (usually around 500 lines of code), easily modifiable, and extendible.
△ Less
Submitted 26 December, 2009;
originally announced December 2009.
-
A unifying approach to picture grammars
Authors:
Matteo Pradella,
Alessandra Cherubini,
Stefano Crespi Reghizzi
Abstract:
Several old and recent classes of picture grammars, that variously extend context-free string grammars in two dimensions, are based on rules that rewrite arrays of pixels. Such grammars can be unified and extended using a tiling based approach, whereby the right part of a rule is formalized by means of a finite set of permitted tiles. We focus on a simple type of tiling,named regional, and define…
▽ More
Several old and recent classes of picture grammars, that variously extend context-free string grammars in two dimensions, are based on rules that rewrite arrays of pixels. Such grammars can be unified and extended using a tiling based approach, whereby the right part of a rule is formalized by means of a finite set of permitted tiles. We focus on a simple type of tiling,named regional, and define the corresponding regional tile grammars. They include both Siromoney's (or Matz's) Kolam grammars and their generalization by Prusa, as well as Drewes's grid grammars. Regionally defined pictures can be recognized with polynomial-time complexity by an algorithm extending the CKY one for strings. Regional tile grammars and languages are strictly included into our previous tile grammars and languages, and are incomparable with Giammarresi-Restivo tiling systems (or Wang systems).
△ Less
Submitted 8 January, 2011; v1 submitted 15 October, 2009;
originally announced October 2009.
-
Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms
Authors:
Marcello M. Bersani,
Carlo A. Furia,
Matteo Pradella,
Matteo Rossi
Abstract:
Complex systems typically have many different parts and facets, with different characteristics. In a multi-paradigm approach to modeling, formalisms with different natures are used in combination to describe complementary parts and aspects of the system. This can have a beneficial impact on the modeling activity, as different paradigms an be better suited to describe different aspects of the sys…
▽ More
Complex systems typically have many different parts and facets, with different characteristics. In a multi-paradigm approach to modeling, formalisms with different natures are used in combination to describe complementary parts and aspects of the system. This can have a beneficial impact on the modeling activity, as different paradigms an be better suited to describe different aspects of the system. While each paradigm provides a different view on the many facets of the system, it is of paramount importance that a coherent comprehensive model emerges from the combination of the various partial descriptions. In this paper we present a technique to model different aspects of the same system with different formalisms, while keeping the various models tightly integrated with one another. In addition, our approach leverages the flexibility provided by a bounded satisfiability checker to encode the verification problem of the integrated model in the propositional satisfiability (SAT) problem; this allows users to carry out formal verification activities both on the whole model and on parts thereof. The effectiveness of the approach is illustrated through the example of a monitoring system.
△ Less
Submitted 29 July, 2009;
originally announced July 2009.
-
A Metric Encoding for Bounded Model Checking (extended version)
Authors:
Matteo Pradella,
Angelo Morzenti,
Pierluigi San Pietro
Abstract:
In Bounded Model Checking both the system model and the checked property are translated into a Boolean formula to be analyzed by a SAT-solver. We introduce a new encoding technique which is particularly optimized for managing quantitative future and past metric temporal operators, typically found in properties of hard real time systems. The encoding is simple and intuitive in principle, but it i…
▽ More
In Bounded Model Checking both the system model and the checked property are translated into a Boolean formula to be analyzed by a SAT-solver. We introduce a new encoding technique which is particularly optimized for managing quantitative future and past metric temporal operators, typically found in properties of hard real time systems. The encoding is simple and intuitive in principle, but it is made more complex by the presence, typical of the Bounded Model Checking technique, of backward and forward loops used to represent an ultimately periodic infinite domain by a finite structure. We report and comment on the new encoding technique and on an extensive set of experiments carried out to assess its feasibility and effectiveness.
△ Less
Submitted 27 July, 2009; v1 submitted 17 July, 2009;
originally announced July 2009.
-
Practical Automated Partial Verification of Multi-Paradigm Real-Time Models
Authors:
Carlo A. Furia,
Matteo Pradella,
Matteo Rossi
Abstract:
This article introduces a fully automated verification technique that permits to analyze real-time systems described using a continuous notion of time and a mixture of operational (i.e., automata-based) and descriptive (i.e., logic-based) formalisms. The technique relies on the reduction, under reasonable assumptions, of the continuous-time verification problem to its discrete-time counterpart.…
▽ More
This article introduces a fully automated verification technique that permits to analyze real-time systems described using a continuous notion of time and a mixture of operational (i.e., automata-based) and descriptive (i.e., logic-based) formalisms. The technique relies on the reduction, under reasonable assumptions, of the continuous-time verification problem to its discrete-time counterpart. This reconciles in a viable and effective way the dense/discrete and operational/descriptive dichotomies that are often encountered in practice when it comes to specifying and analyzing complex critical systems. The article investigates the applicability of the technique through a significant example centered on a communication protocol. More precisely, concurrent runs of the protocol are formalized by parallel instances of a Timed Automaton, while the synchronization rules between these instances are specified through Metric Temporal Logic formulas, thus creating a multi-paradigm model. Verification tests run on this model using a bounded validity checker implementing the technique show consistent results and interesting performances.
△ Less
Submitted 4 July, 2008; v1 submitted 28 April, 2008;
originally announced April 2008.
