ETH Logo

Publications of Carlo A. Furia

Currently submitted and work in progress

(Ask me if you're interested in drafts of these papers.)

Research papers

Theses

Technical reports and reviews

Details

To have a "caf-bib.bib" BibTeX file with all the entries in this page, save the page as "publications.html" and then run the Awk script: 

awk 'BEGIN {bib = 0} /^@[A-Z][a-zA-Z]*\{.+,$/ {if (!bib) {bib = 1}} {if (bib) print $0} /^\}$/ {if (bib) {bib = 0; print "\n"}}' publications.html > caf-bib.bib

Yi Wei, Hannes Roth, Carlo A. Furia, Yu Pei, Alexander Horton, Michael Steindorfer, Martin Nordio, and Bertrand Meyer
Stateful Testing: Finding More Errors in Code and Contracts.
In Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE'11).
Pgg. 440--443, ACM, November 2011.

Abstract
Automated random testing has shown to be an effective approach to finding faults but still faces a major unsolved issue: how to generate test inputs diverse enough to find many faults and find them quickly. Stateful testing, the automated testing technique introduced in this article, generates new test cases that improve an existing test suite. The generated test cases are designed to violate the dynamically inferred contracts (invariants) characterizing the existing test suite. As a consequence, they are in a good position to detect new errors, and also to improve the accuracy of the inferred contracts by discovering those that are unsound.
Experiments on 13 data structure classes totalling over 28,000 lines of code demonstrate the effectiveness of stateful testing in improving over the results of long sessions of random testing: stateful testing found 68.4% new faults and improved the accuracy of automatically inferred contracts to over 99%, with just a 7% time overhead. 

@InProceedings{WRFPHSNM-ASE11,
  author = {Yi Wei and Hannes Roth and Carlo A. Furia and Yu Pei and Alexander Horton and Michael Steindorfer and Martin Nordio and Bertrand Meyer},
  title = {Stateful Testing: Finding More Errors in Code and Contracts},
  booktitle = {Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE'11)},
  editor    = {Perry Alexander and Corina Pasareanu and John Hosking},
  pages = {440--443},
  year = {2011},
  month = {November},
  publisher = {ACM},
  acceptancerate = {43\%}
}

Yu Pei, Yi Wei, Carlo A. Furia, Martin Nordio, and Bertrand Meyer
Code-Based Automated Program Fixing.
In Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE'11).
Pgg. 392--395, ACM, November 2011.

Abstract
Many programmers, when they encounter an error, would like to have the benefit of automatic fix suggestions---as long as they are, most of the time, adequate. Initial research in this direction has generally limited itself to specific areas, such as data structure classes with carefully designed interfaces, and relied on simple approaches.
To provide high-quality fix suggestions in a broad area of applicability, the present work relies on the presence of contracts in the code, and on the availability of dynamic analysis to gather evidence on the values taken by expressions derived from the program text.
The ideas have been built into the AutoFix-E2 automatic fix generator. Applications of AutoFix-E2 to general-purpose software, such as a library to manipulate documents, show that the approach provides an improvement over previous techniques, in particular purely model-based approaches. 

@InProceedings{PWFNM11-ASE11,
  author = {Yu Pei and Yi Wei and Carlo A. Furia and Martin Nordio and Bertrand Meyer},
  title = {Code-Based Automated Program Fixing},
  booktitle = {Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE'11)},
  editor    = {Perry Alexander and Corina Pasareanu and John Hosking},
  pages = {392--395},
  year = {2011},
  month = {November},
  publisher = {ACM},
  acceptancerate = {43\%}
}

Julian Tschannen, Carlo A. Furia, Martin Nordio, and Bertrand Meyer.
Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques.
In 9th International Conference on Software Engineering and Formal Methods (SEFM'11).
Lecture Notes in Computer Science, 7041:382--398, Springer, November 2011.

Abstract
With formal techniques becoming more and more powerful, the next big challenge is making software verification practical and usable. The Eve verification environment contributes to this goal by seamlessly integrating a static prover and an automatic testing tool into a development environment. The paper discusses the general principles behind the integration of heterogeneous verification tools; the peculiar challenges involved in combining static proofs and dynamic testing techniques; and how the combination, implemented in Eve through a blackboard architecture, can improve the user experience with little overhead over usual development practices. Eve is freely available for download. 

@InProceedings{TFNM11-SEFM11,
  author = {Julian Tschannen and Carlo A. Furia and Martin Nordio and Bertrand Meyer},
  title = {Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques},
  booktitle = {9th International Conference on Software Engineering and Formal Methods ({SEFM}'11)},
  pages = {382--398},
  year = {2011},
  editor = {Gilles Barthe and Alberto Pardo and Gerardo Schneider},
  volume = {7041},
  series = {Lecture Notes in Computer Science},
  month = {November},
  publisher = {Springer},
  acceptancerate = {28\%}
}

Carlo A. Furia and Paola Spoletini.
On Relaxing Metric Information in Linear Temporal Logic.
In Proceedings of the 18th International Symposium on Temporal Representation and Reasoning (TIME'11).
Pgg. 72--79, IEEE Computer Society, September 2011.

Abstract
Metric LTL formulas rely on the next operator to encode time distances, whereas qualitative LTL formulas use only the until operator. This paper shows how to transform any metric LTL formula M into a qualitative formula Q, such that Q is satisfiable if and only if M is satisfiable over words with variability bounded with respect to the largest distances used in M (i.e., occurrences of next), but the size of Q is independent of such distances. Besides the theoretical interest, this result can help simplify the verification of systems with time-granularity heterogeneity, where large distances are required to express the coarse-grain dynamics in terms of fine-grain time units. 

@InProceedings{FS11-TIME11,
  author = {Carlo A. Furia and Paola Spoletini},
  title = {On Relaxing Metric Information in Linear Temporal Logic},
  booktitle = {Proceedings of the 18th International Symposium on Temporal Representation and Reasoning (TIME'11)},
  editor    = {Carlo Combi and Martin Leucker and Frank Wolter},
  pages = {72--79},
  year = {2011},
  month = {September},
  publisher = {IEEE Computer Society},
  acceptancerate = {44\%}
}

Marco Trudel, Manuel Oriol, Carlo A. Furia, and Martin Nordio.
Automated Translation of Java Source Code to Eiffel.
In Objects, Components, Models, Patterns. 49th International Conference, TOOLS Europe 2011.
Lecture Notes in Computer Science, 6705:20--35, Springer, June 2011.

Abstract
Reusability is an important software engineering concept actively advocated for the last forty years. While reusability has been addressed for systems implemented using the same programming language, it does not usually handle interoperability with different programming languages. This paper presents a solution for the reuse of Java code within Eiffel programs based on a source-to-source translation from Java to Eiffel. The paper focuses on the critical aspects of the translation and illustrates them by formal means. The translation is implemented in the freely available tool J2Eif; it provides Eiffel replacements for the components of the Java runtime environment, including Java Native Interface services and reflection mechanisms. Our experiments demonstrate the practical usability of the translation scheme and its implementation, and record the performance slow-down compared to custom-made Eiffel applications: automatic translations of java.util data structures, java.io services, and SWT applications can be re-used as Eiffel programs, with the same functionalities as their original Java implementations. 

@InProceedings{TOFN11-TOOLS11,
  author = {Marco Trudel and Manuel Oriol and Carlo A. Furia and Martin Nordio},
  title = {Automated Translation of {J}ava Source Code to {E}iffel},
  booktitle = {Objects, Components, Models, Patterns. 49th International Conference, {TOOLS} Europe 2011},
  pages = {20--35},
  year = {2011},
  editor = {Judith Bishop and Antonio Vallecillo},
  volume = {6705},
  series = {Lecture Notes in Computer Science},
  month = {June},
  publisher = {Springer},
  acceptancerate = {28\%}
}

Yi Wei, Carlo A. Furia, Nikolay Kazmin, and Bertrand Meyer.
Inferring Better Contracts.
In Proceedings of the 33rd International Conference on Software Engineering (ICSE'11).
Pgg. 191--200, ACM, May 2010.

Abstract
Considerable progress has been made towards automatic support for one of the principal techniques available to enhance program reliability: equipping programs with extensive contracts. The results of current contract inference tools are still often unsatisfactory in practice, especially for programmers who already apply some kind of basic Design by Contract discipline, since the inferred contracts tend to be simple assertions---the very ones that programmers find easy to write. We present new, completely automatic inference techniques and a supporting tool, which take advantage of the presence of simple programmer-written contracts in the code to infer sophisticated assertions, involving for example implication and universal quantification.
Applied to a production library of classes covering standard data structures such as linked lists, arrays, stacks, queues and hash tables, the tool is able, entirely automatically, to infer 75% of the complete contracts---contracts yielding the full formal specification of the classes---with very few redundant or irrelevant clauses. 

@InProceedings{WFKM11-ICSE11,
  author = {Yi Wei and Carlo A. Furia and Nikolay Kazmin and Bertrand Meyer},
  title = {Inferring Better Contracts},
  booktitle = {Proceedings of the 33rd International Conference on Software Engineering (ICSE'11)},
  editor    = {Richard N. Taylor and Harald Gall and Nenad Medvidovi{\' c}},
  pages = {191--200},
  year = {2011},
  month = {May},
  publisher = {ACM},
  acceptancerate = {14\%}
}

Carlo A. Furia and Matteo Rossi.
A Theory of Sampling for Continuous-Time Metric Temporal Logic.
ACM Transactions on Computational Logic, 12(1):1--40, October 2010.

Abstract
This article revisits the classical notion of sampling in the setting of real-time temporal logics for the modeling and analysis of systems. The relationship between the satisfiability of Metric Temporal Logic (MTL) formulas over continuous-time models and over discrete-time models is studied. It is shown to what extent discrete-time sequences obtained by sampling continuous-time signals capture the semantics of MTL formulas over the two time domains. The main results apply to "flat" formulas that do not nest temporal operators and can be applied to the problem of reducing the verification problem for MTL over continuous-time models to the same problem over discrete-time, resulting in an automated partial practically-efficient discretization technique. 

@Article{FR10-TOCL10,
  author = {Carlo A. Furia and Matteo Rossi},
  title = {A Theory of Sampling for Continuous-Time Metric Temporal Logic},
  journal = {ACM Transactions on Computational Logic},
  volume = {12},
  number = {1},
  year = {2010},
  pages = {1--40},
  publisher = {ACM},
  month = {October},
  note = {Article 8}
}

Carlo A. Furia and Bertrand Meyer.
Inferring Loop Invariants Using Postconditions.
In Fields of Logic and Computation: Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday.
Lecture Notes in Computer Science, 6300:277--300, Springer, August 2010.

Abstract
One of the obstacles in automatic program proving is to obtain suitable loop invariants. The invariant of a loop is a weakened form of its postcondition (the loop's goal, also known as its contract); the present work takes advantage of this observation by using the postcondition as the basis for invariant inference, using various heuristics such as "uncoupling" which prove useful in many important algorithms. Thanks to these heuristics, the technique is able to infer invariants for a large variety of loop examples. We present the theory behind the technique, its implementation (freely available for download and currently relying on Microsoft Research's Boogie tool), and the results obtained. 

@InProceedings{FM10-YG70-post,
  author = {Carlo A. Furia and Bertrand Meyer},
  title = {Inferring Loop Invariants Using Postconditions},
  booktitle = {Fields of Logic and Computation: Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday},
  pages = {277--300},
  year = {2010},
  editor = {Andreas Blass and Nachum Dershowitz and Wolfgang Reisig},
  volume = {6300},
  series = {Lecture Notes in Computer Science},
  month = {August},
  publisher = {Springer}
}

Carlo A. Furia.
What's Decidable About Sequences?
In Proceedings of the 8th International Symposium on Automated Technology for Verification and Analysis (ATVA'10).
Lecture Notes in Computer Science, 6252:128--142, Springer-Verlag, September 2010.

Abstract
We present a first-order theory of (finite) sequences with integer elements, Presburger arithmetic, and regularity constraints, which can model significant properties of data structures such as lists and queues. We give a decision procedure for the quantifier-free fragment, based on an encoding into the first-order theory of concatenation; the procedure has PSPACE complexity. The quantifier-free fragment of the theory of sequences can express properties such as sortedness and injectivity, as well as Boolean combinations of periodic and arithmetic facts relating the elements of the sequence and their positions (e.g., "for all even i's, the element at position i has value i+3 or 2i"). The resulting expressive power is orthogonal to that of the most expressive decidable logics for arrays. Some examples demonstrate that the fragment is also suitable to reason about sequence-manipulating programs within the standard framework of axiomatic semantics. 

@InProceedings{Fur10-ATVA10,
  author = {Carlo A. Furia},
  title = {What's Decidable About Sequences?},
  booktitle = {Proceedings of the 8th International Symposium on Automated Technology for Verification and Analysis (ATVA'10)},
  pages = {128--142},
  year = {2010},
  editor = {Ahmed Bouajjani and Wei-Ngan Chin},
  volume = {6252},
  series = {Lecture Notes in Computer Science},
  month = {September},
  publisher = {Springer},
  acceptancerate = {41\%}
}

Dino Mandrioli, Stephen Fickas, Carlo A. Furia, Mehdi Jazayeri, Matteo Rossi, and Michal Young.
SCORE: the first student contest on software engineering.
SIGSOFT Software Engineering Notes 35(4):24--30, July 2010.

Abstract
The Student Contest on Software Engineering (SCORE), organized for the first time in conjunction with the International Conference on Software Engineering (ICSE) 2009, attracted 50 student teams from around the world, produced an impressive and varied set of projects, and earned appreciative comments from participants and even from teams who chose not to submit their results to the competition. It was a remarkable success, but not without problems and setbacks. In this article we explain the objectives, constraints, and design philosophy of SCORE, particularly as they distinguish it from the tradition of computer science contests focused more narrowly on programming. We also recount key approaches taken to design and management of this novel kind of contest, the difficulties we met (some still outstanding), and the lessons learned. 

@Article{MFFJRY10-SEN10,
  author =                {Dino Mandrioli and Stephen Fickas and Carlo A. Furia and Mehdi Jazayeri and Matteo Rossi and Michal Young},
  title =                 {{SCORE}: the first student contest on software engineering},
  journal =       {SIGSOFT Software Engineering Notes},
  year =                  {2010},
  volume =        {35},
  number =        {4},
  pages =         {24--30},
  month =         {July}
}

Nadia Polikarpova, Carlo A. Furia, and Bertrand Meyer.
Specifying Reusable Components.
In Proceedings of the 3rd International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'10).
Lecture Notes in Computer Science, 6217:127--141, Springer-Verlag, August 2010.

Abstract
Reusable software components need expressive specifications. This paper outlines a rigorous foundation of model-based contracts, a method to equip classes with strong contracts that support accurate design, implementation, and formal verification of reusable components. Model-based contracts conservatively extend the classic Design by Contract approach with a notion of model, which underpins the precise definitions of such concepts as abstract object equivalence and specification completeness. Experiments applying model-based contracts to libraries of data structures suggest that the method enables accurate specification of practical software.

Notes
Some technical details, that are omitted in the paper, can be found in this technical report. 

@InProceedings{PFM10-VSTTE10,
  author = {Nadia Polikarpova and Carlo A. Furia and Bertrand Meyer},
  title = {Specifying Reusable Components},
  booktitle = {Proceedings of the 3rd International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE'10)},
  pages = {127--141},
  year = {2010},
  editor = {Gary T. Leavens and Peter O'Hearn and Sriram Rajamani},
  volume = {6217},
  series = {Lecture Notes in Computer Science},
  month = {August},
  publisher = {Springer},
  acceptancerate = {36\%}
}

Yi Wei, Yu Pei, Carlo A. Furia, Lucas S. Silva, Stefan Buchholz, Bertrand Meyer, and Andreas Zeller.
Automated Fixing of Programs with Contracts.
In Proceedings of the 19th International Symposium on Software Testing and Analysis (ISSTA'10).
Pgg. 61--72, ACM, July 2010.

Abstract
In program debugging, finding a failing run is only the first step; what about correcting the fault? Can we automate the second task as well as the first? The AutoFix-E tool automatically generates and validates fixes for software faults. The key insights behind AutoFix-E are to rely on contracts present in the software to ensure that the proposed fixes are semantically sound, and on state diagrams using an abstract notion of state based on the boolean queries of a class.
Out of 42 faults found by an automatic testing tool in two widely used Eiffel libraries, AutoFix-E proposes successful fixes for 16 faults. Submitting some of these faults to experts shows that several of the proposed fixes are identical or close to fixes proposed by humans. 

@InProceedings{WPFSBMZ10-ISSTA10,
  author = {Yi Wei and Yu Pei and Carlo A. Furia and Lucas S. Silva and Stefan Buchholz and Bertrand Meyer and Andreas Zeller},
  title = {Automated Fixing of Programs with Contracts},
  booktitle = {Proceedings of the 19th International Symposium on Software Testing and Analysis (ISSTA'10)},
  editor    = {Paolo Tonella and Alessandro Orso},
  pages = {61--72},
  year = {2010},
  month = {July},
  publisher = {ACM},
  acceptancerate = {23\%}
}

Carlo A. Furia, Dino Mandrioli, Angelo Morzenti, and Matteo Rossi.
Modeling Time in Computing: a taxonomy and a comparative survey.
ACM Computing Surveys, 42(2):1--59, February 2010.

Abstract
The increasing relevance of areas such as real-time and embedded systems, pervasive computing, hybrid systems control, and biological and social systems modeling is bringing a growing attention to the temporal aspects of computing, not only in the computer science domain, but also in more traditional fields of engineering.
This article surveys various approaches to the formal modeling and analysis of the temporal features of computer-based systems, with a level of detail that is also suitable for nonspecialists. In doing so, it provides a unifying framework, rather than just a comprehensive list of formalisms.
The article first lays out some key dimensions along which the various formalisms can be evaluated and compared. Then, a significant sample of formalisms for time modeling in computing are presented and discussed according to these dimensions. The adopted perspective is, to some extent, historical, going from "traditional" models and formalisms to more modern ones. 

@Article{FMMR10-CSUR10,
  author = {Carlo A. Furia and Dino Mandrioli and Angelo Morzenti and Matteo Rossi},
  title = {Modeling Time in Computing: a taxonomy and a comparative survey},
  journal = {ACM Computing Surveys},
  volume = {42},
  number = {2},
  year = {2010},
  pages = {1--59},
  publisher = {ACM},
  month = {February},
  note = {Article 6}
}

Luca Cavallaro, Elisabetta Di Nitto, Carlo A. Furia, and Matteo Pradella.
A Tile-based Approach for Self-assembling Service Compositions.
In Proceedings of the 15th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'10).
Pgg. 43--52, IEEE, March 2010.

Abstract
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. 

@InProceedings{CDFP10-ICECCS10,
  author = {Luca Cavallaro and Elisabetta {Di Nitto} and Carlo A. Furia and Matteo Pradella},
  title = {A Tile-based Approach for Self-assembling Service Compositions},
  booktitle = {Proceedings of the 15th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'10)},
  pages = {43--52},
  year = {2010},
  month = {March},
  publisher = {IEEE},
  acceptancerate = {23\%}
}

Silvia Bindelli, Elisabetta Di Nitto, Carlo A. Furia, and Matteo Rossi.
Using Compositionality to Formally Model and Analyze Systems Built of a High Number of Components.
In Proceedings of the 15th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'10).
Pgg. 85--94, IEEE, March 2010.

Abstract
When dependability of systems with a large number of components is a concern, being able to model and analyze their properties, especially non-functional ones, in a formal and automated way becomes essential. Often, however, the application of formal methods and automated reasoning is seen by practitioners as complex and time consuming. Compositional techniques can help modify this belief.
In this paper we show how a compositional modeling and verification technique can be applied to the analysis of distributed systems with numerous interacting nodes. We automate the proof by exploiting a SAT-based tool. We demonstrate the validity of the resulting approach by applying it to an autonomic service-based system that manages, in a coordinated peer-to-peer manner, electricity consumption in a geographical area. In particular, we show that in this case the time needed for performing the proof is remarkably shorter than in the case in which we adopt a non-compositional approach. 

@InProceedings{BDFR10-ICECCS10,
  author = {Silvia Bindelli and Elisabetta {Di Nitto} and Carlo A. Furia and Matteo Rossi},
  title = {Using Compositionality to Formally Model and Analyze Systems Built of a High Number of Components},
  booktitle = {Proceedings of the 15th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'10)},
  pages = {85--94},
  year = {2010},
  month = {March},
  publisher = {IEEE},
  acceptancerate = {23\%}
}

Marcello M. Bersani, Carlo A. Furia, Matteo Pradella, and Matteo Rossi.
Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms.
In Proceedings of the 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM'09).
Pgg. 13--22, IEEE Computer Society Press, November 2009.

Abstract
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 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 can be better suited to describe different aspects of complex systems. 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. Our approach leverages the flexibility provided by a bounded satisfiability checker to encode the verification problem of the integrated model in the Boolean 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.

Notes
Some technical details, that are omitted in the paper, can be found in this technical report. 

@InProceedings{BFPR09-SEFM09,
  author = {Marcello M. Bersani and Carlo A. Furia and Matteo Pradella and Matteo Rossi},
  title = {Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms},
  booktitle = {Proceedings of the 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM'09)},
  pages = {13--22},
  year = {2009},
  month = {November},
  publisher = {IEEE Computer Society Press},
  acceptancerate = {35\%}
}

Carlo A. Furia, Matteo Pradella, and Matteo Rossi.
Comments on "Temporal Logics for Real-Time System Specification".
ACM Computing Surveys, 41(2):1--5, February 2009.

Abstract
The article "Temporal Logics for Real-Time System Specification" surveys some of the relevant literature dealing with the use of temporal logics for the specification of real-time systems. Unfortunately, it introduces some imprecisions that mightcreate some confusion in the reader. While a certain degree of informality is certainly useful when addressing a broad audience, imprecisions can negatively impact the legibility of the exposition. We clarify some of its remarks on a few topics, in an effort to contribute to the usefulness of the survey for the reader.

Notes
Publication timeline: Received September 2005; revised July 2007, April 2008; accepted April 2008. 

@Article{FPR09-CSUR09,
  author = {Carlo A. Furia and Matteo Pradella and Matteo Rossi},
  title = {Comments on ``{T}emporal Logics for Real-Time System Specification''},
  journal = {ACM Computing Surveys},
  volume = {41},
  number = {2},
  year = {2009},
  pages = {1--5},
  publisher = {ACM},
  month = {February},
  note = {Extended version as Technical Report 2008.7, Dipartimento di Elettronica e Informazione, Politecnico di Milano, April 2008}
}

Carlo A. Furia and Paola Spoletini.
Practical Efficient Modular Linear-Time Model-Checking.
In Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA'08).
Lecture Notes in Computer Science, 5311:408--417, Springer-Verlag, October 2008.

Abstract
This paper shows how the modular structure of composite systems can guide the state-space exploration in explicit-state linear-time model-checking and make it more efficient in practice. Given a composite system where every module has input and output variables --- and variables of different modules can be connected --- a total ordering according to which variables are generated is determined, through heuristics based on graph-theoretical analysis of the modular structure. The technique is shown to outperform standard exploration techniques (that do not take the modular structure information into account) by several orders of magnitude in experiments with Spin models of MTL formulas. 

@InProceedings{FS08-ATVA08,
  author = {Carlo A. Furia and Paola Spoletini},
  title = {Practical Efficient Modular Linear-Time Model-Checking},
  booktitle = {Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA'08)},
  pages = {408--417},
  year = {2008},
  editor = {Sungdeok (Steve) Cha and Jin-Young Choi and Monzoo Kim and Insup Lee and Mahesh Viswanathan},
  volume = {5311},
  series = {Lecture Notes in Computer Science},
  month = {October},
  publisher = {Springer-Verlag},
  acceptancerate = {34\%}
}

Carlo A. Furia and Matteo Rossi.
MTL with Bounded Variability: Decidability and Complexity.
In Proceedings of the 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'08).
Lecture Notes in Computer Science, 5215:109--123, Springer-Verlag, September 2008.

Abstract
This paper investigates the properties of Metric Temporal Logic (MTL) over models in which time is dense but phenomena are constrained to have bounded variability. Contrary to the case of generic dense-time behaviors, MTL is proved to be fully decidable over models with bounded variability, if the variability bound is given. In these decidable cases, MTL complexity is shown to match that of simpler decidable logics such as MITL. On the contrary, MTL is undecidable if all behaviors with variability bounded by some generic constant are considered, but with an undecidability degree that is lower than in the case of generic behaviors.

Notes
Some technical details, that are omitted in the paper, can be found in this technical report. 

@InProceedings{FR08-FORMATS08,
  author = {Carlo A. Furia and Matteo Rossi},
  title = {{MTL} with Bounded Variability: Decidability and Complexity},
  booktitle = {Proceedings of the 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'08)},
  pages = {109--123},
  year = {2008},
  editor = {Franck Cassez and Claude Jard},
  volume = {5215},
  series = {Lecture Notes in Computer Science},
  month = {September},
  publisher = {Springer-Verlag},
  acceptancerate = {45\%}
}

Carlo A. Furia, Matteo Pradella, and Matteo Rossi.
Practical Automated Partial Verification of Multi-Paradigm Real-Time Models.
In Proceedings of the 10th International Conference on Formal Engineering Methods (ICFEM'08).
Lecture Notes in Computer Science, 5256:298--317, Springer-Verlag, October 2008.

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. 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. 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 satisfiability checker implementing the technique show consistent results and interesting performances.

Notes
Some technical details, that are omitted in the paper, can be found in this technical report. 

@InProceedings{FPR08-ICFEM08,
  author = {Carlo A. Furia and Matteo Pradella and Matteo Rossi},
  title = {Practical Automated Partial Verification of Multi-Paradigm Real-Time Models},
  booktitle = {Proceedings of the 10th International Conference on Formal Engineering Methods (ICFEM'08)},
  pages = {298--317},
  year = {2008},
  editor = {Shaoying Liu and Tom Maibaum and Keijiro Araki},
  volume = {5256},
  series = {Lecture Notes in Computer Science},
  month = {October},
  publisher = {Springer-Verlag},
  acceptancerate = {32\%}
}

Carlo A. Furia, Marco Mazzucchelli, Paola Spoletini, and Mara Tanelli.
Towards the Exhaustive Verification of Real-Time Aspects in Controller Implementation.
In Proceedings of the 9th IEEE International Symposium on Computer-Aided Control System Design (CACSD'08).
Pgg. 1265--1270, IEEE Press, September 2008.

Abstract
In industrial applications, the number of final products endowed with real-time automatic control systems that manage safety-critical situations has dramatically increased. Thus, it is of growing importance that the control system design flow encompasses also its translation into software code and its embedding into a hardware and software network. In this paper, a tool-supported approach to the formal analysis of real-time aspects in controller implementation is proposed. The analysis can ensure that some desired properties of the control loop are preserved in its implementation on a distributed architecture. Moreover, the tool provides as output information which can be used to approach straightforwardly some design problems, such as hardware sizing in the final implementation.

Notes
Several technical details, that are omitted in the paper, can be found in this technical report. 

@InProceedings{FMST08-CACSD08,
  author =                {Carlo A. Furia and Marco Mazzucchelli and Paola Spoletini and Mara Tanelli},
  title =                 {Towards the Exhaustive Verification of Real-Time Aspects in Controller Implementation},
  booktitle = {Proceedings of the 9th IEEE International Symposium on Computer-Aided Control System Design (CACSD'08)},
  pages = {1265--1270},
  year = {2008},
  month = {September},
  publisher = {IEEE Press},
  note = {CACSD'08 is part of the 2nd IEEE Multi-conference on Systems and Control}
}

Carlo A. Furia and Paola Spoletini.
Tomorrow and All Our Yesterdays: MTL Satisfiability over the Integers.
In Proceedings of the 5th International Colloquium on Theoretical Aspects of Computing (ICTAC'08).
Lecture Notes in Computer Science, 5160:126--140, Springer-Verlag, September 2008.

Abstract
We investigate the satisfiability problem for metric temporal logic (MTL) with both past and future operators over linear discrete bi-infinite time models isomorphic to the integer numbers, where time is unbounded both in the future and in the past. We provide a technique to reduce satisfiability over the integers to satisfiability over the well-known mono-infinite time model of natural numbers, and we show how to implement the technique through an automata-theoretic approach. We also prove that MTL satisfiability over the integers is EXPSPACE-complete, hence the given algorithm is optimal in the worst case.

Notes
Some technical details, that are omitted in the paper, can be found in this technical report. 

@InProceedings{FS08-ICTAC08,
  author = {Carlo A. Furia and Paola Spoletini},
  title = {Tomorrow and All Our Yesterdays: {MTL} Satisfiability over the Integers},
  booktitle = {Proceedings of the 5th International Colloquium on Theoretical Aspects of Computing (ICTAC'08)},
  pages = {126--140},
  year = {2008},
  editor = {John S. Fitzgerald and Anne E. Haxthausen and Husnu Yenigun},
  volume = {5160},
  series = {Lecture Notes in Computer Science},
  month = {September},
  publisher = {Springer-Verlag},
  acceptancerate = {38\%}
}

Carlo A. Furia, Matteo Pradella, and Matteo Rossi.
Automated Verification of Dense-Time MTL Specifications via Discrete-Time Approximation.
In Proceedings of the 15th International Symposium on Formal Methods (FM'08).
Lecture Notes in Computer Science, 5014:132--147, Springer-Verlag, May 2008.

Abstract
This paper presents a verification technique for dense-time MTL based on discretization. The technique reduces the validity problem of MTL formulas from dense to discrete time, through the notion of sampling invariance, introduced in previous work [FR06]. Since the reduction is from an undecidable problem to a decidable one, the technique is necessarily incomplete, so it fails to provide conclusive answers for some formulas. The paper discusses this shortcoming and hints at how it can be mitigated in practice. The verification technique has been implemented on top of the Zot tool for discrete-time bounded validity checking; the paper also reports on in-the-small experiments with the tool, which show some results that are promising in terms of performance.

Notes
Some technical details, that are omitted in the paper, can be found in this technical report. 

@InProceedings{FPR08-FM08,
  author = {Carlo A. Furia and Matteo Pradella and Matteo Rossi},
  title = {Automated Verification of Dense-Time {MTL} Specifications via Discrete-Time Approximation},
  booktitle = {Proceedings of the 15th International Symposium on Formal Methods (FM'08)},
  pages = {132--147},
  year = {2008},
  editor = {Jorge Cu{\'e}llar and Tom Maibaum and Kaisa Sere},
  volume = {5014},
  series = {Lecture Notes in Computer Science},
  month = {May},
  publisher = {Springer-Verlag},
  acceptancerate = {21\%}
}

Carlo A. Furia and Matteo Rossi.
No Need To Be Strict: on the expressiveness of metric temporal logics with (non-)strict operators.
Bulletin of the European Association for Theoretical Computer Science, 92:150--160, June 2007.

Abstract
The until modality of temporal logic "A until B" is called strict in its first argument when it does not constrain the value of the first argument A at the instant at which the formula is evaluated. In this paper, we show that linear metric temporal logics with bounded until modalities that are non-strict in the first argument are as expressive as those with strict modalities, when interpreted over non-Zeno dense-time models. 

@Article{FR07-BEATCS,
  author =                {Carlo A. Furia and Matteo Rossi},
  title =                 {No Need To Be Strict: on the expressiveness of metric temporal logics with (non-)strict operators},
  journal =       {Bulletin of the European Association for Theoretical Computer Science},
  year =                  {2007},
  volume =        {92},
  pages =         {150--160},
  month = {June}
}

Carlo A. Furia and Matteo Rossi.
On the Expressiveness of MTL Variants over Dense Time.
In Proceedings of the 5th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'07).
Lecture Notes in Computer Science, 4763:163--178, Springer-Verlag, October 2007.

Abstract
The basic modal operator bounded until of Metric Temporal Logic (MTL) comes in several variants. In particular it can be strict (when it does not constrain the current instant) or not, and matching (when it requires its two arguments to eventually hold together) or not. This paper compares the relative expressiveness of the resulting MTL variants over dense time. We prove that the expressiveness is not affected by the variations when considering non-Zeno interpretations and arbitrary nesting of temporal operators. On the contrary, the expressiveness changes for flat (i.e., without nesting) formulas, or when Zeno interpretations are allowed.

Notes
Some technical details, that are omitted in the paper, can be found in this technical report. 

@InProceedings{FR07-FORMATS07,
  author = {Carlo A. Furia and Matteo Rossi},
  title = {On the Expressiveness of {MTL} Variants over Dense Time},
  booktitle = {Proceedings of the 5th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'07)},
  pages = {163--178},
  year = {2007},
  editor = {Jean-Fran{\c c}ois Raskin and P. S. Thiagarajan},
  volume = {4763},
  series = {Lecture Notes in Computer Science},
  month = {October},
  publisher = {Springer-Verlag},
  acceptancerate = {45\%}
}

Carlo A. Furia, Matteo Rossi, Dino Mandrioli, and Angelo Morzenti.
Automated Compositional Proofs for Real-Time Systems.
Theoretical Computer Science, 376(3):164--184, May 2007.

Abstract
We present a framework for formally proving that the composition of the behaviors of the different parts of a complex, real-time system ensures a desired global specification of the overall system. The framework is based on a simple compositional rely/guarantee circular inference rule, plus a methodology concerning the integration of the different parts into a whole system. The reference specification language is the TRIO metric linear temporal logic.
The novelty of our approach with respect to existing compositional frameworks --- most of which do not deal explicitly with real-time requirements --- consists mainly in its generality and abstraction from any assumptions about the underlying computational model and from any semantic characterizations of the temporal logic language used in the specification. Moreover, the framework deals equally well with continuous and discrete time. It is supported by a tool, implemented on top of the proof-checker PVS, to perform deduction-based verification through theorem-proving of modular real-time axiom systems.
As an example of application, we show the verification of a real-time version of the old-fashioned but still relevant "benchmark" of the dining philosophers problem.

Notes 

@Article{FRMM07-TCS07,
  author =                {Carlo A. Furia and Matteo Rossi and Dino Mandrioli and Angelo Morzenti},
  title =                 {Automated Compositional Proofs for Real-Time Systems},
  journal =       {Theoretical Computer Science},
  year =                  {2007},
  volume =        {376},
  number =        {3},
  pages =         {164--184}
}

Carlo A. Furia, Matteo Rossi, and Dino Mandrioli.
Modeling the Environment in Software-Intensive Systems.
In Proceedings of the Workshop on Modeling in Software Engineering (MISE'07), May 2007.
A Workshop of the 29th International Conference on Software Engineering (ICSE'07).

Abstract
In this paper we argue that the modeling activity in the development of software-intensive systems should formalize as much as possible of the environment in which the application being developed operates. We also show that a rich formal model of the environment helps developers clearly state requirements that might typically be considered intrinsically informal (or non-formalizable in general). To illustrate this point, we show how a requirement for "orderly safe traffic" in a traffic system can be modeled, and we briefly discuss the benefits thereof. 

@InProceedings{FRM07-MISE07,
  author = {Carlo A. Furia and Matteo Rossi and Dino Mandrioli},
  title = {Modeling the Environment in Software-Intensive Systems},
  booktitle = {Proceedings of the Workshop on Modeling in Software Engineering (MISE'07)},
  year = {2007},
  month = {May},
  note = {A Workshop of the 29th International Conference on Software Engineering (ICSE'07)},
  acceptancerate = {43\%}
}

Carlo A. Furia, Angelo Morzenti, Matteo Pradella, and Matteo Rossi.
Comments on "A Temporal Logic for Real-Time System Specification".
IEEE Transactions on Software Engineering, 32(6):424--427, June 2006. (Comments paper).

Abstract
The paper "An Interval Logic for Real-Time System Specification" 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.

Notes
The paper comments on: R. Mattolini and P. Nesi, "A Temporal Logic for Real-Time System Specification". IEEE Transactions on Software Engineering, 27(3):208--227, March 2001. 

@Article{FMPR06-TSE06comments,
  author =                {Carlo A. Furia and Angelo Morzenti and Matteo Pradella and Matteo G. Rossi},
  title =                 {Comments on ``{A} Temporal Logic for Real-Time System Specification''},
  journal =       {IEEE Transactions on Software Engineering},
  year =                  {2006},
  volume =        {32},
  number =        {6},
  pages =         {424--427},
  month =         {June},
  note =          {Comments paper}
}

Carlo A. Furia and Matteo Rossi.
Integrating Discrete- and Continuous-Time Metric Temporal Logics Through Sampling.
In Proceedings of the 4th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'06).
Lecture Notes in Computer Science, 4202:215--229, Springer-Verlag, September 2006.

Abstract
Real-time systems usually encompass parts that are best described by a continuous-time model, such as physical processes under control, together with other components that are more naturally formalized by a discrete-time model, such as digital computing modules. Describing such systems in a unified framework based on metric temporal logic requires to integrate formulas which are interpreted over discrete and continuous time.
In this paper, we tackle this problem with reference to the metric temporal logic TRIO, that admits both a discrete-time and a continuous-time semantics. We identify sufficient conditions under which TRIO formulas have a consistent truth value when moving from continuous-time to discrete-time interpretations, or vice versa. These conditions basically involve the restriction to a proper subset of the TRIO language and a requirement on the finite variability over time of the basic items in the specification formulas. We demonstrate the approach with an example of specification and verification.

Notes
Some technical details, that are omitted in the paper, can be found in this technical report. 

@InProceedings{FR06-FORMATS06,
  author = {Carlo A. Furia and Matteo Rossi},
  title = {Integrating Discrete- and Continuous-Time Metric Temporal Logics Through Sampling},
  booktitle = {Proceedings of the 4th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'06)},
  pages = {215--229},
  year = {2006},
  editor = {Eugene Asarin and Patricia Bouyer},
  volume = {4202},
  series = {Lecture Notes in Computer Science},
  month = {September},
  publisher = {Springer-Verlag},
  acceptancerate = {44\%}
}

Carlo A. Furia, Matteo Rossi, Dino Mandrioli, and Angelo Morzenti.
Automated Compositional Proofs for Real-Time Systems.
In Proceedings of the 8th International Conference on Fundamental Approaches to Software Engineering (FASE'05).
Lecture Notes in Computer Science, 3442:326--340, Springer-Verlag, March 2005.

Abstract
We present a framework for formally proving that the composition of the behaviors of the different parts of a complex, real-time system ensures a desired global specification of the overall system. The framework is based on a simple compositional rely/guarantee circular inference rule, plus a small set of conditions concerning the integration of the different parts into a whole system. The reference specification language is the TRIO metric linear temporal logic.
The novelty of our approach with respect to existing compositional frameworks --- most of which do not deal explicitly with real-time requirements --- consists mainly in its generality and abstraction from any assumptions about the underlying computational model and from any semantic characterizations of the temporal logic language used in the specification. Moreover, the framework deals equally well with continuous and discrete time. It is supported by a tool, implemented on top of the proof-checker PVS, to perform deduction-based verification through theorem-proving of modular real-time axiom systems.
As an example of application, we show the verification of a real-time version of the old-fashioned but still relevant "benchmark" of the dining philosophers problem.

Notes
Unfortunately, the paper published in the proceedings contains a (minor) error. In fact, a variation of the time progression operator ->>, including the current instant and denoted as ->>_i, was quickly introduced and used to specify the case study. However, for this variation of the operator the inference rule of Proposition 1 no longer holds, as it is. The reason for that is basically that Lemma 1 cannot be proved, since we can no longer rule out the accumulation of the future intervals of the NowOn operator (to see this, consider a right-open interval and what happens on its right boundary). Nonetheless, the case study can still be specified using the base ->> operator, with really minimal changes. Here, of course, you find the patched versions of the paper. 

@InProceedings{FRMM05-FASE05,
  author = {Carlo A. Furia and Matteo Rossi and Dino Mandrioli and Angelo Morzenti},
  title = {Automated Compositional Proofs for Real-Time Systems},
  booktitle = {Proceedings of the 8th International Conference on Fundamental Approaches to Software Engineering (FASE'05)},
  pages = {326--340},
  year = {2005},
  editor = {Maura Cerioli},
  volume = {3442},
  series = {Lecture Notes in Computer Science},
  month = {March},
  publisher = {Springer-Verlag},
  note = {Conference held as part of the Joint European Conferences on Theory and Practice of Software (ETAPS'05)},
  acceptancerate = {22\%}
}

Andrea Matta, Carlo A. Furia, and Matteo Rossi.
Semi-Formal and Formal Models Applied to Flexible Manufacturing Systems.
In Proceedings of the 19th International Symposium on Computer and Information Sciences (ISCIS'04).
Lecture Notes in Computer Science, 3280:718--728, Springer-Verlag, October 2004.

Abstract
Flexible Manufacturing Systems (FMSs) are adopted to process different goods in different mix ratios allowing firms to react quickly and efficiently to changes in products and production targets (e.g. volumes, etc.). Due to their high costs, FMSs require careful design, and their performance must be precisely evaluated before final deployment. To support and guide the design phase, this paper presents a UML semi-formal model for FMSs that captures the most prominent aspects of these systems. For a deeper analysis, two refinements could then be derived from the UML intermediate description: simulation components for "empirical" analysis, and an abstract formal model that is suitable for formal verification. In this paper we focus on the latter, based on the TRIO temporal logic. In particular, we hint at a methodology to derive TRIO representations from the corresponding UML descriptions, and apply it to the case of FMSs. A subset of the resulting formal model is then used to verify, through logic deduction, a simple property of the FMS. 

@InProceedings{MFR04-ISCIS04,
  author = {Andrea Matta and Carlo A. Furia and Matteo Rossi},
  title = {Semi-Formal and Formal Models Applied to Flexible Manufacturing Systems},
  booktitle = {Proceedings of the 19th International Symposium on Computer and Information Sciences (ISCIS'04)},
  pages = {718--728},
  year = {2004},
  editor = {Cevdet Aykanat and Tu{\v g}rul Dayar and {\. I}brahim K{\"o}rpeo{\v g}lu},
  volume = {3280},
  series = {Lecture Notes in Computer Science},
  month = {October},
  publisher = {Springer-Verlag},
  acceptancerate = {29\%}
}

Carlo A. Furia, and Matteo Rossi.
A Compositional Framework for Formally Verifying Modular Systems.
In Proceedings of the International Workshop on Test and Analysis of Component Based Systems (TACoS'04).
Electronic Notes in Theoretical Computer Science, 116:185--198, Elsevier, March 2004.

Abstract
We present a tool-supported framework for proving that the composition of the behaviors of the separate parts of a complex system ensures a desired global property of the overall system. A compositional inference rule is formally introduced and encoded in the logic of the PVS theorem prover. Methodological considerations on the usage of the inference rule are presented, and the framework is then used to prove a meaningful property of a simple, but significant, control system.

Notes
This paper presents sketchily the inference rule also shown, more extensively and within a broader framework, in the FASE'05 paper, and then discusses some details of how it has been implemented in the PVS tools for TRIO. 

@InProceedings{FR04-TACoS04,
  author = {Carlo A. Furia and Matteo Rossi},
  title = {A Compositional Framework for Formally Verifying Modular Systems},
  booktitle = {Proceedings of the International Workshop on Test and Analysis of Component Based Systems (TACoS'04)},
  pages = {185--198},
  year = {2004},
  volume = {116},
  series = {Electronic Notes in Theoretical Computer Science},
  month = {January},
  publisher = {Elsevier}
}

Carlo Alberto Furia.
Scaling Up the Formal Analysis of Real-Time Systems.
PhD Thesis.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, May 2007.

Abstract
We develop techniques and methods to scale the application of formal methods up to large and heterogenous systems. Our solution focuses on real-time systems, and develops along the two aspects of compositionality and integration.
In the first part, we provide a compositional framework for specifying and verifying properties of modular systems, written using metric temporal logics with a descriptive approach. The framework consists in technical as well as methodological features. On the technical side, we provide an array of compositional inference rules to deduce facts about the composition of modules from facts about each component in isolation. Each rule has different features that make it more suitable for certain classes of systems. We also provide a general methodology to guide the formal specification of modular systems, and the application of the inference rules to verify them.
In the second part, we consider the problem of integration for systems with both discrete-time and continuous-time components. We provide suitable conditions under which metric temporal logic formulas have a consistent truth value whether they are interpreted in discrete or in continuous time, and we identify a language subset that meets these conditions. We also characterize the conditions and the language subset with detail. Our approach to integration permits the verification of global properties of heterogenous systems. 

@PhdThesis{Fur07-PhD,
  author = {Carlo Alberto Furia},
  title = {Scaling Up the Formal Analysis of Real-Time Systems},
  school = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
  year = {2007},
  month = {May}
}

Carlo Alberto Furia.
Compositional Proofs for Real-Time Modular Systems.
Master's Thesis (Tesi di Laurea).
Politecnico di Milano, December 2003.

Notes
The "Laurea degree thesis" is basically an extended version of the Master's thesis, and it's entirely written in English.

Folklore note
When I graduated, the degree I earned was simply called "Laurea", and concluded five years of university studies (thus basically corresponding to a Master's). After a reform of public Italian university, five-year-long degrees were split into a three-year-long one plus a two-year-long one, similarly to a Bachelor and Master's. However, the three-year-long degree was now called "Laurea", whereas the one obtained after two more years passed through the names "Laurea Specialistica" (specialized laurea) and the silly-sounding (at least to me) "Laurea Magistrale" (magisterial laurea). I don't know to what names it will be changed to in the future, but I just wanted to explain to which "Laurea" I'm referring to here. 

@MastersThesis{Fur03-Laurea,
  author = {Carlo Alberto Furia},
  title = {Compositional Proofs for Real-Time Modular Systems},
  school = {Politecnico di Milano},
  year = {2003},
  month = {December},
  note = {(Tesi di Laurea)}
}

Carlo Alberto Furia.
Compositional Proofs for Real-Time Modular Systems.
Master's Thesis.
University of Illinois at Chicago, October 2003. 

@MastersThesis{Fur03-MS,
  author = {Carlo Alberto Furia},
  title = {Compositional Proofs for Real-Time Modular Systems},
  school = {University of Illinois at Chicago},
  year = {2003},
  month = {October}
}

Carlo A. Furia.
A Survey of Multi-Tape Automata
arXiv.org > cs > 1205.0178, May 2012.

Abstract
This paper summarizes the fundamental expressiveness, closure, and decidability properties of various finite-state automata classes with multiple input tapes. It also includes an original algorithm for the intersection of one-way nondeterministic finite-state automata. 

@Misc{F12-TR-01052012,
  author =                {Carlo A. Furia},
  title =                 {A Survey of Multi-Tape Automata},
  howpublished = {\url{http://arxiv.org/abs/1205.0178}},
  month =         {May},
  year =          {2012}
}

Martin Nordio, H.-Christian Estler, Carlo A. Furia, and Bertrand Meyer
Collaborative Software Development on the Web.
arXiv.org > cs > 1105.0768, September 2011.

Abstract
Software development environments (IDEs) have not followed the IT industry's inexorable trend towards distribution. They do too little to address the problems raised by today's increasingly distributed projects; neither do they facilitate collaborative and interactive development practices. A consequence is the continued reliance of today's IDEs on paradigms such as traditional configuration management, which were developed for earlier modes of operation and hamper collaborative projects. This contribution describes a new paradigm: cloud-based development, which caters to the specific needs of distributed and collaborative projects. The CloudStudio IDE embodies this paradigm by enabling developers to work on a shared project repository. Configuration management becomes unobtrusive; it replaces the explicit update-modify-commit cycle by interactive editing and real-time conflict tracking and management. A case study involving three teams of pairs demonstrates the usability of CloudStudio and its advantages for collaborative software development over traditional configuration management practices. 

@Misc{NEFM-TR-20110919,
  author =                {Martin Nordio and  H.-Christian Estler and Carlo A. Furia and Bertrand Meyer},
  title =                 {Collaborative Software Development on the Web},
  howpublished = {\url{http://arxiv.org/abs/1105.0768}},
  month =         {September},
  year =          {2011}
}

Yi Wei, Hannes Roth, Carlo A. Furia, Yu Pei, Alexander Horton, Michael Steindorfer, Martin Nordio, and Bertrand Meyer
Stateful Testing: Finding More Errors in Code and Contracts.
arXiv.org > cs > 1108.1068, August 2011.

Abstract
Automated random testing has shown to be an effective approach to finding faults but still faces a major unsolved issue: how to generate test inputs diverse enough to find many faults and find them quickly. Stateful testing, the automated testing technique introduced in this article, generates new test cases that improve an existing test suite. The generated test cases are designed to violate the dynamically inferred contracts (invariants) characterizing the existing test suite. As a consequence, they are in a good position to detect new errors, and also to improve the accuracy of the inferred contracts by discovering those that are unsound.
Experiments on 13 data structure classes totalling over 28,000 lines of code demonstrate the effectiveness of stateful testing in improving over the results of long sessions of random testing: stateful testing found 68.4% new faults and improved the accuracy of automatically inferred contracts to over 99%, with just a 7% time overhead. 

@Misc{WRFPHSNM-TR-20110804,
  author =                {Yi Wei and Hannes Roth and Carlo A. Furia and Yu Pei and Alexander Horton and Michael Steindorfer and Martin Nordio and Bertrand Meyer},
  title =                 {Stateful Testing: Finding More Errors in Code and Contracts},
  howpublished = {\url{http://arxiv.org/abs/1108.1068}},
  month =         {August},
  year =          {2011}
}

Julian Tschannen, Carlo A. Furia, Martin Nordio, and Bertrand Meyer
Verifying Eiffel Programs with Boogie.
arXiv.org > cs > 1106.4700, June 2011.

Abstract
Static program verifiers such as Spec#, Dafny, jStar, and VeriFast define the state of the art in automated functional verification techniques. The next open challenges are to make verification tools usable even by programmers not fluent in formal techniques. This paper presents AutoProof, a verification tool that translates Eiffel programs to Boogie and uses the Boogie verifier to prove them. In an effort to be usable with real programs, AutoProof fully supports several advanced object-oriented features including polymorphism, inheritance, and function objects. AutoProof also adopts simple strategies to reduce the amount of annotations needed when verifying programs (e.g., frame conditions). The paper illustrates the main features of AutoProof's translation, including some whose implementation is underway, and demonstrates them with examples and a case study. 

@Misc{TFNM11-TR-20110624,
  author =                {Julian Tschannen and Carlo A. Furia and Martin Nordio and Bertrand Meyer},
  title =                 {Verifying {E}iffel Programs with {B}oogie},
  howpublished = {\url{http://arxiv.org/abs/1106.4700}},
  month =         {June},
  year =          {2011}
}

Carlo A. Furia
QFIS -- A verifier for the theory of quantifier-free integer sequences.
User manual, v. 1.0, 2011--2012. 

@Misc{QFIS-manual,
  author =                {Carlo A. Furia},
  title =                 {{QFIS} -- A verifier for the theory of quantifier-free integer sequences},
  howpublished = {User manual, v.~1.0},
  year =          {2011--2012}
}

Yu Pei, Yi Wei, Carlo A. Furia, Martin Nordio, and Bertrand Meyer
Code-Based Automated Program Fixing.
arXiv.org > cs > 1102.1059, February 2011, revised August 2011.

Abstract
Many programmers, when they encounter an error, would like to have the benefit of automatic fix suggestions---as long as they are, most of the time, adequate. Initial research in this direction has generally limited itself to specific areas, such as data structure classes with carefully designed interfaces, and relied on simple approaches.
To provide high-quality fix suggestions in a broad area of applicability, the present work relies on the presence of contracts in the code, and on the availability of dynamic analysis to gather evidence on the values taken by expressions derived from the program text.
The ideas have been built into the AutoFix-E2 automatic fix generator. Applications of AutoFix-E2 to general-purpose software, such as a library to manipulate documents, show that the approach provides an improvement over previous techniques, in particular purely model-based approaches. 

@Misc{PWFNM11-TR-20110205,
  author =                {Yu Pei and Yi Wei and Carlo A. Furia and Martin Nordio and Bertrand Meyer},
  title =                 {Code-Based Automated Program Fixing},
  howpublished = {\url{http://arxiv.org/abs/1102.1059}},
  month =         {February},
  year =          {2011},
  note = {Revised in August 2011}
}

Carlo A. Furia.
Review of The Calculus of Computation by A. R. Bradley and Z. Manna.
ACM SIGACT News, 42(1):32--35, March 2011. 

@Article{Fur11-Review-BradleyManna,
  author =                {Carlo A. Furia},
  title =                 {Review of \emph{The Calculus of Computation} by {A.\ R.\ Bradley} and {Z.\ Manna}},
  journal =       {ACM SIGACT News},
  year =                  {2011},
  volume =        {42},
  number =        {1},
  pages =         {32--35},
  month =         {March}
}

Carlo A. Furia, Alberto Leva, Martina Maggio, and Paola Spoletini.
A control-theoretical methodology for the scheduling problem.
arXiv.org > cs > 1009.3455, September 2010.

Abstract
This paper presents a novel methodology to develop scheduling algorithms. The scheduling problem is phrased as a control problem, and control-theoretical techniques are used to design a scheduling algorithm that meets specific requirements. Unlike most approaches to feedback scheduling, where a controller integrates a "basic" scheduling algorithm and dynamically tunes its parameters and hence its performances, our methodology essentially reduces the design of a scheduling algorithm to the synthesis of a controller that closes the feedback loop. This approach allows the re-use of control-theoretical techniques to design efficient scheduling algorithms; it frames and solves the scheduling problem in a general setting; and it can naturally tackle certain peculiar requirements such as robustness and dynamic performance tuning. A few experiments demonstrate the feasibility of the approach on a real-time benchmark. 

@Misc{FLMS10-TR-20092010,
  author =                {Carlo A. Furia and Alberto Leva and Martina Maggio and Paola Spoletini},
  title =                 {A control-theoretical methodology for the scheduling problem},
  howpublished = {\url{http://arxiv.org/abs/1009.3455}},
  month =         {September},
  year =          {2010}
}

Nadia Polikarpova, Carlo A. Furia, and Bertrand Meyer.
Specifying Reusable Components.
arXiv.org > cs > 1003.5777, March 2010.

Abstract
Reusable software components need well-defined interfaces, rigorously and completely documented features, and a design amenable both to reuse and to formal verification; all these requirements call for expressive specifications. This paper outlines a rigorous foundation to model-based contracts, a methodology to equip classes with expressive contracts supporting the accurate design, implementation, and formal verification of reusable components. Model-based contracts conservatively extend the classic Design by Contract by means of expressive models based on mathematical notions, which underpin the precise definitions of notions such as abstract equivalence and specification completeness. Preliminary experiments applying model-based contracts to libraries of data structures demonstrate the versatility of the methodology and suggest that it can introduce rigorous notions, but still intuitive and natural to use in practice. 

@Misc{PFM10-TR-30032010,
  author =                {Nadia Polikarpova and Carlo A. Furia and Bertrand Meyer},
  title =                 {Specifying Reusable Components},
  howpublished = {\url{http://arxiv.org/abs/1003.5777}},
  month =         {March},
  year =          {2010}
}

Paul Z. Kolano, Carlo A. Furia, Richard A. Kemmerer, and Dino Mandrioli.
Refinement and Verification of Real-Time Systems.
arXiv.org > cs > 1002.1796, February 2010.

Abstract
This paper discusses highly general mechanisms for specifying the refinement of a real-time system as a collection of lower level parallel components that preserve the timing and functional requirements of the upper level specification. These mechanisms are discussed in the context of ASTRAL, which is a formal specification language for real-time systems. Refinement is accomplished by mapping all of the elements of an upper level specification into lower level elements that may be split among several parallel components. In addition, actions that can occur in the upper level are mapped to actions of components operating at the lower level. This allows several types of implementation strategies to be specified in a natural way, while the price for generality (in terms of complexity) is paid only when necessary. The refinement mechanisms are first illustrated using a simple digital circuit; then, through a highly complex phone system; finally, design guidelines gleaned from these specifications are presented. 

@Misc{KFKM10-TR-09022010,
  author =                {Paul Z. Kolano and Carlo A. Furia and Richard A. Kemmerer and Dino Mandrioli},
  title =                 {Refinement and Verification of Real-Time Systems},
  howpublished = {\url{http://arxiv.org/abs/1002.1796}},
  month =         {February},
  year =          {2010}
}

Carlo A. Furia.
What's Decidable About Sequences?
arXiv.org > cs > 1001.2100, January 2010.

Abstract
We present a first-order theory of sequences with integer elements, Presburger arithmetic, and regular constraints, which can model significant properties of data structures such as arrays and lists. We give a decision procedure for the quantifier-free fragment, based on an encoding into the first-order theory of concatenation; the procedure has PSPACE complexity. The quantifier-free fragment of the theory of sequences can express properties such as sortedness and injectivity, as well as Boolean combinations of periodic and arithmetic facts relating the elements of the sequence and their positions (e.g., "for all even i's, the element at position i has value i+3 or 2i"). The resulting expressive power is orthogonal to that of the most expressive decidable logics for arrays. Some examples demonstrate that the fragment is also suitable to reason about sequence-manipulating programs within the standard framework of axiomatic semantics. 

@Misc{F10-TR-13012010,
  author =                {Carlo A. Furia},
  title =                 {What's Decidable About Sequences?},
  howpublished = {\url{http://arxiv.org/abs/1001.2100}},
  month =         {January},
  year =          {2010}
}

Carlo A. Furia and Matteo Rossi.
A Theory of Sampling for Continuous-time Metric Temporal Logic.
arXiv.org > cs > 0911.5642, November 2009.

Abstract
This paper revisits the classical notion of sampling in the setting of real-time temporal logics for the modeling and analysis of systems. The relationship between the satisfiability of Metric Temporal Logic (MTL) formulas over continuous-time models and over discrete-time models is studied; more precisely, it is shown to what extent discrete-time sequences obtained by sampling continuous-time signals capture the semantics of MTL formulas over the two time domains. These results are applied to the problem of reducing the verification problem for MTL over continuous-time models to the same problem over discrete-time, resulting in an automated partial practically-efficient discretization technique. 

@Misc{FR09-TR-30112009,
  author =                {Carlo A. Furia and Matteo Rossi},
  title =                 {A Theory of Sampling for Continuous-time {M}etric {T}emporal {L}ogic},
  howpublished = {\url{http://arxiv.org/abs/0911.5642}},
  month =         {November},
  year =          {2009}
}

Carlo A. Furia and Bertrand Meyer.
Inferring Loop Invariants using Postconditions.
arXiv.org > cs > 0909.0884, September 2009.

Abstract
One of the obstacles in automatic program proving is to obtain suitable loop invariants. The invariant of a loop is a weakened form of its postcondition (the loop's goal, also known as its contract); the present work takes advantage of this observation by using the postcondition as the basis for invariant inference, using various heuristics such as "uncoupling" which prove useful in many important algorithms. Thanks to these heuristics, the technique is able to infer invariants for a large variety of loop examples. We present the theory behind the technique, its implementation (freely available for download and currently relying on Microsoft Research's Boogie tool), and the results obtained. 

@Misc{FM09-TR-04092009,
  author =                {Carlo A. Furia and Bertrand Meyer},
  title =                 {Inferring Loop Invariants using Postconditions},
  howpublished = {\url{http://arxiv.org/abs/0909.0884}},
  month =         {September},
  year =          {2009}
}

Marcello M. Bersani, Carlo A. Furia, Matteo Pradella, and Matteo Rossi.
Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms.
arXiv.org > cs > 0907.5074, July 2009.

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 can 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. 

@Misc{BFPR09-TR-29072009,
  author =                {Marcello M. Bersani and Carlo A. Furia and Matteo Pradella and Matteo Rossi},
  title =                 {Integrated Modeling and Verification of Real-Time Systems through Multiple Paradigms},
  howpublished = {\url{http://arxiv.org/abs/0907.5074}},
  month =         {July},
  year =          {2009}
}

Carlo A. Furia and Paola Spoletini.
On Relaxing Metric Information in Linear Temporal Logic.
arXiv.org > cs > 0906.4711, June 2009, revised April 2010, April 2011, June 2011.

Abstract
Metric LTL formulas rely on the next operator to encode time distances, whereas qualitative LTL formulas use only the until operator. This paper shows how to transform any metric LTL formula M into a qualitative formula Q, such that Q is satisfiable if and only if M is satisfiable over words with variability bounded with respect to the largest distances used in M (i.e., occurrences of next), but the size of Q is independent of such distances. Besides the theoretical interest, this result can help simplify the verification of systems with time-granularity heterogeneity, where large distances are required to express the coarse-grain dynamics in terms of fine-grain time units.

Notes
The April 2010 version of the report is a major revision that eliminates the exponential blow-up in the transformation from M to Q (present in the June 2009 version of the report). The April 2011 version further refines the main result of the paper in considering the satisfiability of Q over unconstrained words. The June 2011 version is a minor revision which fixes some typos. 

@Misc{FS09-TR-RelaxingMetricLTL,
  author =                {Carlo A. Furia and Paola Spoletini},
  title =                 {On Relaxing Metric Information in Linear Temporal Logic},
  howpublished = {\url{http://arxiv.org/abs/0906.4711}},
  month =         {June},
  year =          {2009},
  note = {Last revised in June 2011}
}

Carlo A. Furia and Matteo Rossi.
MTL with Bounded Variability: Decidability and Complexity.
Technical Report 2008.10.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, May 2008.

Abstract
This paper investigates the properties of Metric Temporal Logic (MTL) over models in which time is dense but phenomena are constrained to have bounded variability. Contrary to the case of generic dense-time behaviors, MTL is proved to be fully decidable over models with bounded variability, if the variability bound is given. In these decidable cases, MTL complexity is shown to match that of simpler decidable logics such as MITL. On the contrary, MTL is undecidable if all behaviors with variability bounded by some generic constant are considered, but with an undecidability degree that is lower than in the case of generic behaviors. 

@TechReport{FR08-TR2008-10,
  author =                {Carlo A. Furia and Matteo Rossi},
  title =                 {{MTL} with Bounded Variability: Decidability and Complexity},
  institution =  {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
  year =                  {2008},
  number =        {2008.10},
  month =         {May}
}

Carlo A. Furia, Matteo Pradella, and Matteo Rossi.
Practical Automated Partial Verification of Multi-Paradigm Real-Time Models.
arXiv.org > cs > 0804.4383, April 2008.

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. 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. 

@Misc{FPR08-TR-28042008,
  author =                {Carlo A. Furia and Matteo Pradella and Matteo Rossi},
  title =                 {Practical Automated Partial Verification of Multi-Paradigm Real-Time Models},
  howpublished = {\url{http://arxiv.org/abs/0804.4383}},
  month =         {April},
  year =          {2008}
}

Carlo A. Furia and Paola Spoletini.
MTL Satisfiability over the Integers.
Technical Report 2008.2.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, February 2008.

Abstract
We investigate the satisfiability problem for metric temporal logic (MTL) with both past and future operators over linear discrete bi-infinite time models --- where time is unbounded both in the future and in the past --- isomorphic to the integer numbers. We provide a technique to reduce satisfiability over the integers to satisfiability over the well-known mono-infinite time model of natural numbers, and we show how to implement the technique through an automata-theoretic approach. We also prove that MTL satisfiability over the integers is EXPSPACE-complete, hence the given algorithm is optimal in the worst case. 

@TechReport{FS08-TR2008-2,
  author =                {Carlo A. Furia and Paola Spoletini},
  title =                 {{MTL} Satisfiability over the Integers},
  institution =  {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
  year =                  {2008},
  number =        {2008.2},
  month =         {February}
}

Carlo A. Furia, Marco Mazzucchelli, Paola Spoletini, and Mara Tanelli.
Towards the Exhaustive Verification of Real-Time Aspects in Controller Implementation.
Technical Report 2008.1.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, January 2008.

Abstract
In industrial applications, the number of final products endowed with real-time automatic control systems that manage critical situations as far as human safety is concerned has dramatically increased. Thus, it is of growing importance that the control system design flow encompasses also its translation into software code and its embedding into a hardware and software network. In this paper, a tool-supported approach to the formal analysis of real-time aspects in controller implementation is proposed. The analysis can ensure that some desired properties of the control loop are preserved in its implementation on a distributed architecture. Moreover, the information extracted automatically from the model can also be used to approach straightforwardly some design problems, such as the hardware sizing in the final implementation. 

@TechReport{FMST08-TR2008-1,
  author =                {Carlo A. Furia and Marco Mazzucchelli and Paola Spoletini and Mara Tanelli},
  title =                 {Towards the Exhaustive Verification of Real-Time Aspects in Controller Implementation},
  institution =  {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
  year =                  {2008},
  number =        {2008.1},
  month =         {January}
}

Carlo A. Furia and Matteo Rossi.
On the Expressiveness of MTL Variants over Dense Time.
Technical Report 2007.41.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, May 2007.

Abstract
The basic modal operator bounded until of Metric Temporal Logic (MTL) comes in several variants. In particular it can be strict (when it does not constraint the current instant) or not, and matching (when it requires its two arguments to eventually hold together) or not. This paper compares the relative expressiveness of the resulting MTL variants over dense time. We prove that the expressiveness is not affected by the variations when considering non-Zeno interpretations and arbitrary nesting of temporal operators. On the contrary, the expressiveness changes for flat (i.e., without nesting) formulas, or when Zeno interpretations are allowed. 

@TechReport{FR07-TR2007-41,
  author =                {Carlo A. Furia and Matteo Rossi},
  title =                 {On the Expressiveness of {MTL} Variants over Dense Time},
  institution =  {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
  year =                  {2007},
  number =        {2007.41},
  month =         {May}
}

Carlo A. Furia, Matteo Pradella, and Matteo Rossi.
Dense-Time MTL Verification Through Sampling.
Technical Report 2007.37.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, April 2007.

Abstract
This paper presents a verification technique for dense-time MTL based on discretization. The technique reduces the validity problem of MTL formulas from dense to discrete time, through the notion of sampling invariance, introduced in previous work [FR06]. Since the reduction is from an undecidable problem to a decidable one, the technique is necessarily incomplete, so it fails to provide conclusive answers on some problem instances. The paper discusses this shortcoming and hints at how it can be mitigated in practice. The verification technique has been implemented on top of a tool for discrete-time bounded validity checking; the paper also reports on in-the-small experiments with the tool, which show some promising results. 

@TechReport{FPR07-TR2007-37,
  author =                {Carlo A. Furia and Matteo Pradella and Matteo Rossi},
  title =                 {Dense-Time {MTL} Verification Through Sampling},
  institution =  {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
  year =                  {2007},
  number =        {2007.37},
  month =         {April}
}

Carlo A. Furia, Dino Mandrioli, Angelo Morzenti, and Matteo Rossi.
Modeling Time in Computing: a taxonomy and a comparative survey.
arXiv.org > cs > 0807.4132, July 2008.
(A preliminary version appeared as Technical Report 2007.22, Dipartimento di Elettronica e Informazione, Politecnico di Milano, January 2007).

Abstract
The increasing relevance of areas such as real-time and embedded systems, pervasive computing, hybrid systems control, and biological and social systems modeling is bringing a growing attention to the temporal aspects of computing, not only in the computer science domain, but also in more traditional fields of engineering.
This article surveys various approaches to the formal modeling and analysis of the temporal features of computer-based systems, with a level of detail that is suitable also for non-specialists. In doing so, it provides a unifying framework, rather than just a comprehensive list of formalisms.
The paper first lays out some key dimensions along which the various formalisms can be evaluated and compared. Then, a significant sample of formalisms for time modeling in computing are presented and discussed according to these dimensions. The adopted perspective is, to some extent, historical, going from "traditional" models and formalisms to more modern ones. 

@Misc{FMMR08-TR-25072008,
  author =                {Carlo A. Furia and Dino Mandrioli and Angelo Morzenti and Matteo Rossi},
  title =                 {Modeling Time in Computing: a taxonomy and a comparative survey},
  howpublished = {\url{http://arxiv.org/abs/0807.4132}},
  month =         {July},
  year =          {2008},
  note = {(A preliminary version appeared as Technical Report 2007.22, Dipartimento di Elettronica e Informazione, Politecnico di Milano, January 2007)}
}

Carlo Alberto Furia.
Discrete Meets Continuous, Again.
Technical Report 2006.77.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, December 2006.

Abstract
This report collects some contributions about issues related to the notion of sampling invariance that has been introduced in [FR05,FR06], of which the present report can therefore be considered a follow-up and a complement.
In particular: we compare the expressiveness of the language R-Z-TRIO against that of MTL (and MITL), by also showing a result about the expressiveness of non-strict temporal operators; we characterize behaviors of bounded variability and formulas that preserve the bounded variability requirement; we compare the notion of sampling invariance with that of digitization [HMP92]; we discuss how to describe the runs of a timed automata with R-Z-TRIO formulas; we provide an example of application of the sampling invariance techniques to a simple verification problem; we summarize several related works on the expressiveness, decidability, and complexity of formalisms that are somewhat related to the R-Z-TRIO temporal logic. 

@TechReport{Fur06-TR2006-77,
  author =                {Carlo Alberto Furia},
  title =                 {Discrete Meets Continuous, Again},
  institution =  {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
  year =                  {2006},
  number =        {2006.77},
  month =         {December}
}

Carlo Alberto Furia.
Compositionality Made Up.
Technical Report 2006.76.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, December 2006.

Abstract
This paper develops some methods and techniques for the practical use of compositionality to prove the correctness of modular systems, with reference to the metric temporal logic TRIO. It advocates a "lightweight" approach to compositionality, driven by the specifics of the system under development, where methodology is as important as technical solutions. 

@TechReport{Fur06-TR2006-76,
  author =                {Carlo Alberto Furia},
  title =                 {Compositionality Made Up},
  institution =  {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
  year =                  {2006},
  number =        {2006.76},
  month =         {December}
}

Carlo A. Furia, Matteo Rossi, Elisabeth A. Strunk, Dino Mandrioli, and John C. Knight.
Raising Formal Methods To The Requirements Level.
Technical Report 2006.64.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, November 2006.
Also: Technical Report CS-2006-24, Department of Computer Science, University of Virginia.

Abstract
In contrast with a formal notion of specification, requirements are often considered an informal entity. In a companion paper [SFRKM06], we have proposed a reference model that provides a clear distinction between requirements and specification, a distinction not based on the degree of formality. Using that notion of requirements, this paper shows how requirements as well as specifications can be formalized.
The formalization of requirements allows one to "lift" the well-known practices of formal analysis and verification from the specification/implementation level up to the highest level of abstraction in the development of a software product. In particular, we show how a formal validity argument can be constructed, proving that the formal specification satisfies its formal requirements. These ideas are demonstrated in an illustrative example based on a runway incursion prevention system, which was also partially presented in [SFRKM06]. Although our results and methods are of general applicability, we focus especially on the real-time aspects of the example; in order to support real-time formalization and reasoning, we exploit the ArchiTRIO formal language in a UML-like environment. 

@TechReport{FRSMK06-TR2006-64,
  author =                {Carlo A. Furia and Matteo Rossi and Elisabeth A. Strunk and Dino Mandrioli and John C. Knight},
  title =                 {Raising Formal Methods To The Requirements Level},
  institution =  {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
  year =                  {2006},
  number =        {2006.64},
  month =         {November},
  note =          {Also: Technical Report CS-2006-24, Department of Computer Science, University of Virginia}
}

Elisabeth A. Strunk, Carlo A. Furia, Matteo Rossi, John C. Knight, and Dino Mandrioli.
The Engineering Roles of Requirements and Specification.
Technical Report CS-2006-21.
Department of Computer Science, University of Virginia, October 2006.
Also: Technical Report 2006.61, Dipartimento di Elettronica e Informazione, Politecnico di Milano

Abstract
The distinction between requirements and specification is often confused in practice. This obstructs the system validation process, because it is unclear what exactly should be validated, and against what it should be validated. The reference model of Gunter et al. addresses this difficulty by providing a framework within which requirements can be distinguished from specification. It separates world phenomena from machine phenomena. However, it does not explain how the characterization can be used to help assure system validity.
In this paper, we enhance the reference model to account for certain key elements that are necessary to expose and clarify the distinction and the link between requirements and specification. We use the enhanced version to present a more refined picture of validity, where validation has two steps that can be undertaken separately. We use this picture to question whether the "what the system will do, not how it will do it" paradigm is useful in describing how to construct a specification, and propose an alternative. Finally, we present the requirements and specification for an illustrative example based on a runway incursion prevention system, with the ArchiTRIO formal language in a UML-like environment, to show how this might be done in practice. 

@TechReport{SFRKM06-TR2006-61,
  author =                {Elisabeth A. Strunk and Carlo A. Furia and Matteo Rossi and John C. Knight and Dino Mandrioli},
  title =                 {The Engineering Roles of Requirements and Specification},
  institution =  {Department of Computer Science, University of Virginia},
  year =                  {2006},
  number =        {CS-2006-21},
  month =         {October},
  note =          {Also: Technical Report 2006.61, Dipartimento di Elettronica e Informazione, Politecnico di Milano}
}

Carlo Alberto Furia.
Quantum Informatics: A Survey.
Technical Report 2006.16.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, January 2006.

Abstract
We survey the emerging field of quantum computing by showing its motivations and founding principles, and by presenting the most significant results in some selected areas. In particular, we outline the topics of quantum information, quantum algorithms, quantum cryptography, quantum finite automata, quantum error correction, and the physical realizations of quantum computing systems. 

@TechReport{Fur06-TR2006-16,
  author = {Carlo Alberto Furia},
  title = {Quantum Informatics: A Survey},
  institution = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
  year = {2006},
  number = {2006.16},
  month = {January}
}

Carlo A. Furia, and Matteo Rossi.
When Discrete Met Continuous: on the integration of discrete- and continuous-time metric temporal logics.
Technical Report 2005.44.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, October 2005.

Abstract
Real-time systems usually encompass parts that are best described by a continuous-time model, such as physical processes under control, together with other components that are more naturally formalized by a discrete-time model, such as digital computing modules. Describing such systems in a unified framework based on metric temporal logic requires to integrate formulas which are interpreted over discrete and continuous time.
In this paper, we tackle this problem with reference to the metric temporal logic TRIO, that admits both a discrete-time and a continuous-time semantics. We identify sufficient conditions for a TRIO specification to be invariant under change of time model from discrete to continuous and vice versa. These conditions basically involve the restriction to a proper subset of the TRIO language (which we call TRIOsi) and a requirement on the finite variability over time of the values of the basic items that constitute the formulas of the specification. A specification which is invariant can then be verified entirely under the simpler discrete-time model, with the results of the verification holding for the continuous-time model as well.
We believe that this approach is general enough to be easily extendible to other temporal logics of comparable expressive power. 

@TechReport{FR05-TR2005-44,
  author = {Carlo A. Furia and Matteo Rossi},
  title = {When Discrete Met Continuous: on the integration of discrete- and continuous-time metric temporal logics},
  institution = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
  year = {2005},
  number = {2005.44},
  month = {October}
}

Carlo Alberto Furia.
A Compositional World: a survey of recent works on compositionality in formal methods.
Technical Report 2005.22.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, March 2005.

Abstract
We survey the most significant literature about compositional techniques for concurrent and real-time system verification. We especially focus on abstract frameworks for rely/guarantee compositionality that handles circularity, but also consider different developments. 

@TechReport{Fur05-TR2005-22,
  author = {Carlo Alberto Furia},
  title = {A Compositional World: a survey of recent works on compositionality in formal methods},
  institution = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
  year = {2005},
  number = {2005.22},
  month = {March}
}

Carlo A. Furia, Dino Mandrioli, Angelo Morzenti, Matteo Pradella, Matteo Rossi, and Pierluigi San Pietro.
Higher-Order TRIO.
Technical Report 2004.28.
Dipartimento di Elettronica e Informazione, Politecnico di Milano, September 2004.

Notes
This paper introduces the basics about a higher-order extension of the first-order metric temporal logic TRIO. 

@TechReport{FMMPRS04-TR2004-28,
  author = {Carlo A. Furia and Dino Mandrioli and Angelo Morzenti and Matteo Pradella and Matteo Rossi and Pierluigi {San Pietro}},
  title = {Higher-Order {TRIO}},
  institution = {Dipartimento di Elettronica e Informazione, Politecnico di Milano},
  year = {2004},
  number = {2004.28},
  month = {September}
}

Valid XHTML 1.0 Strict