Bibliografia
[ACE+03] M. Alpuente, M. Comini, S. Escobar, M. Falaschi, and S. Lucas. Abstract Diagnosis of Functional Programs. In Proc. of LOPSTR 2002, LNCS 2664, pp 1--16, Springer-Verlag 2003.
[ACF01] Declarative Debugging of Functional Logic Programs. M. Alpuente, F. Correa and M. Falaschi. Proc.of WRS 2001, ENTCS 57, 2001.
[Ber00] The Foundations of Esterel. G. Berry. Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 2000,
[BGM95] Modeling Real-time in Concurrent Constraint Programming. F.S. de Boer, M. Gabbrielli and M.C. Meo. Proc. of ILPS'95. ACM Press, pp 528--542, 1995.
[BGM00] A Timed Concurrent Constraint Language. F.S. de Boer, M. Gabbrielli, and M.C. Meo. I&C, vol. 161, 2000.
[BMP03] D. Bresolin, A. Montanari, and G. Puppis. Time granularities and ultimately periodic automata. TR 24, DIMI, Università di Udine, Italy, 2003.
[CC92] P. Cousot and R. Cousot. Abstract Interpretation Frameworks. Journal of Logic and Computation, 2(4):511--549, 1992.
[CGL01a] M. Comini, R. Gori, and G. Levi. Assertion based Inductive Verification Methods for Logic Programs. In A. K. Seda, editor, Proceedings of MFCSIT'2000, volume 40 of ENTCS, pages 1--18, North Holland, 2001. Elsevier Science Publishers.
[CGL01b] M. Comini, R. Gori, and G. Levi. How to Transform an Analyzer into a Verifier. In proc. of LPAR'01, LNAI 2250, pp 595--609, Berlin, 2001. Springer-Verlag.
[CGLV03] M. Comini, R. Gori, G. Levi, and P. Volpe. Abstract Interpretation based Verification of Logic Programs. SCP, 49(1--3):89--123, 2003.
[CGP99] Model Checking. E.M. Clarke and O. Grumberg and D. Peled. MIT Press, 1999.
[CLMV97] Abstract Diagnosis. M. Comini, G. Levi, M. C. Meo and G. Vitiello. Special Issue on Synthesis, Transformation and Analysis of Logic Programs, JLP 39(1-3):43--93, 1999.
[Com98] M. Comini. An Abstract Interpretation Framework for Semantics and Diagnosis of Logic Programs. PhD thesis, Dipartimento di Informatica, Universita di Pisa, Pisa, Italy, 1998.
[Cou03] Verification by abstract interpretation. P. Cousot. In Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, LNCS 2772, pp 243-268, Springer 2003.
[Dam96] Abstract Interpretation and Partition Refinement for Model Checking. D.R. Dams. PhD thesis, Eindhoven University, 1996.
[Dem03] S. Demri. LTL over integer periodicity constraints. Technical Report LSV-03-13, Laboratoire de Specification et Verification, CNRS, Cachan Cedex France, 2003.
[DLM01] Calendars, Time Granularities, and Automata. U. Dal Lago and A. Montanari. Proc. of SSTD 2001: 7th Int. Symp. on Spatial and Temporal Databases, LNCS 2121, pp. 279-298, 2001.
[DMP03] Ugo Dal Lago, Angelo Montanari, and Gabriele Puppis. Towards compact and tractable automaton-based representations of time granularity. In Proc. of the 8th ICTCS, LNCS 2841, pp 72--85, Springer, 2003.
[EM04] Jerome Euzenat and Angelo Montanari. Time granularity. In Michael Fisher, Dov Gabbay, and Lluis Vila, editors, Handbook of Temporal Reasoning in AI. Elsevier Science, Vol 1 in the Foundations of AI Series, 2004.
[FGR96] G. File', R. Giacobazzi, and F. Ranzato. A Unifying View on Abstract Domain Design. ACM Comp Surveys, 28(2):333--336, 1996.
[FM03] Massimo Franceschet and Angelo Montanari. Branching within time: an expressively complete and elementarily decidable temporal logic for time granularity. Research on Language and Computation, 1(3-4):229--263, 2003.
[FM04] Massimo Franceschet and Angelo Montanari. Temporalized logics and automata for time granularity. TPLP, 4(5-6), 2004.
[FMR04] Massimo Franceschet, Angelo Montanari, and Maarten de Rijke. Model checking for combined logics with an application to mobile systems. Automated Software Eng., 11(3), 2004.
[FPV00] Modeling Timed Concurrent Systems in a Temporal Concurrent Constraint Language-I. M. Falaschi, A. Policriti and A. Villanueva. ENTCS, vol. 48, 2000.
[FPV01] Time Limited Model Checking. M. Falaschi, A. Policriti and A. Villanueva. In Proc. of the Specification, Analysis and Verification for Emerging Technologies in Comp. Logic (SAVE'01), 2001.
[FV03] Automatic Verification of Timed Concurrent Constraint Programs. M. Falaschi and A. Villanueva. Submitted for publication.
[GJSB95] Programming in hybrid constraint languages. V. Gupta, R. Jagadeesan, V. Saraswat and D. Bobrow. Hybrid Systems II. LNCS 999, Springer Verlag,1995.
[GR95] R. Giacobazzi and F. Ranzato. Functional dependencies and Moore-set completions of abstract interpretations and semantics. In Proc. of ILPS'95, pp 321--335, The MIT Press 1995.
[GS97] R. Giacobazzi and F. Scozzari. Intuitionistic Implication in
Abstract Interpretation. In Proc. of PLILP'97, LNCS 1292, pp 175--189, Springer-Verlag 1997.
[Hol97] The model checker SPIN. G.J. Holzmann. IEEE Transactions on Software Engineering, 23:279--295, 1997.
[McM93] Symbolic Model Checking: An Approach to the State Explosion Problem. K.L. McMillan. Kluwer Academic, 1993.
[Mil83] A Calculi for Synchrony and Asynchrony. R. Milner. TCS 25(3):267--310, 1983.
[MLAH99] Difference Decision Diagrams. J. Moller, J. Lichtenberg, H. Andersen and H. Hulgaard. Proc. of the 13th Intl. Workshop on Computer Logic Science, LNCS 1683, pp 111-125, Sprinter 1999.
[Mo96] Metric and layered temporal logic for time granularity. A. Montanari ILLC Dissertation Series 1996-02, Institute for Logic, Language and Computation, Univ. of Amsterdam, 1996.
[MP04] A. Montanari and G. Puppis. Monadic second-order theories of branching structures. TR 01, DIMI, Università di Udine, Italy, 2004. (http://www.dimi.uniud.it/~montana/rr01.ps).
[MPP99] Angelo Montanari, Adriano Peron, and Alberto Policriti. Decidable theories of omega-layered metric temporal structures. Logic journal of the IGPL, 7(1):79--102, 1999.
[MPP02] Angelo Montanari, Adriano Peron, and Alberto Policriti. Extending Kamp's theorem to model time granularity. JLC, 12(4):641--678, 2002.
[MSV02] Angelo Montanari, Guido Sciavicco, and Nicola Vitacolonna. Decidability of interval temporal logics over split-frames via granularity. In Proc. of the European Conf. on Logic in AI, LNAI 2424, pp 259--270. Springer, 2002.
[MPSS95] A Logical view of Concurrent Constraint Programming. N.P. Mendler, P. Panangaden, P.J. Scott and R.A.G. Seely. NJC, vol. 2(2):181--220, 1995.
[Pel94] Combining partial order reduction with on-the-fly model checking. D. Peled. Proc. of CAV'94, pp. 377--390, 1994.
[PV01] A Temporal Concurrent Constraint Programming Calculus. C. Palamidessi and F.D. Valencia. In Proc. of the 7th Int. Conf. PPDP (CP01), LNCS 2239(4):302-. 2001.
[Sa89a] Concurrent Constraint Programming Languages. V.A. Saraswat. PhD thesis, Carnegie-Mellon University, MIT Press, 1991.
[Sha82] Algorithmic Program Debugging. E. Y. Shaphiro. ACM Distinguished Dissertation, MIT Press, 1982.
[SJG94b] Programming in Timed Concurrent Constraint Programming. V.A. Saraswat, R. Jagadeesan and V. Gupta. Constraint Programming:Proc. 1993 (NATO ASI Parnu Estonia), Springer Verlag, pp. 361--410, 1994.
[SJG95] Time Default Concurrent Constraint Programming. V.A.Saraswat, R.Jagadeesan and V.Gupta. JSC 22(5-6):475--520, 1996.
[SRP91] Semantics Foundations of Concurrent Constraint Programming. V.A. Saraswat, M. Rinard, and P. Panangaden. In Proc. of POPL. ACM Press, 1991.
[Tho03] Constructing infinite graphs with a decidable MSO-theory. Thomas Wolfgang. Proc. of the 28th International Symposium on Mathematical Foundations of Computer Science, LNCS 2747, Sprinter 2003.
[Val90] A stubborn attack on state explosion. A. Valmari. Proc. CAV'90, 1990.
[Var97] What makes modal logic so robustly decidable? M.Y. Vardi. In Descriptive Complexity and Finite Models, AMS, 1997.
[VW94] Reasoning about infinite computations. M.Y. Vardi and P. Wolper. I&C 115(1):1--37, 1994.
WP1: Analisi Statica/Domini Astratti Task UD1.1 In letteratura si possono trovare molti domini sviluppati per l'analisi. Questi sono stati sviluppati come opportuno bilanciamento fra precisione e tempo di esecuzione delle operazioni. Molte di queste soluzioni sono state progettate "ad hoc" senza tener conto di metodi di combinazione/raffinamento sviluppati nel mondo dell'Int. Astr. [CC92,FGR96,GR95,GS97]. Inoltre anche per le soluzioni sviluppate sistematicamente la necessità di ragionevoli performance nel calcolo di punto fisso orienta in generale lo sviluppo verso un sacrificio di precisione. I frameworks di debugging e di verifica astratta (basati su Int. Astr.) non devono calcolare punti fissi nei domini astratti ma solo singoli passi dell'operatore delle conseguenze immediate astratte. Quindi nello sviluppare domini da usare per questi tool l'enfasi può essere posta più sulla precisione che non sull'efficienza. In questo ambito intendiamo sviluppare nuovi domini (a partire da quelli "base" finora utilizzati in [CLMV97,CGLV03,CGL01b]), mediante le tecniche sistematiche di combinazione e raffinamento citate prima, che portino un aumento di precisione negli strumenti di diagnosi e verifica, mantenendo una performance ragionevole. Ci aspettiamo che degli esempi molto interessanti possano venire dalla combinazione di domini usati per l'analisi con domini usati per il type-checking. Domini di questo genere non saranno interessanti dal punto di vista dell'analisi ma sicuramente saranno un buon terreno per aiutare i programmatori nel trovare (staticamente) errori senza costringerli a dover fornire in modo eccessivamente dettagliato la specifica intesa del loro programma. Data la struttura parametrica con cui è stato scritto il codice degli strumenti già realizzati i nuovi prototipi si potranno ottenere semplicemente re-implementando solo le operazioni canoniche del nuovo dominio. WP3: Testing e Debugging Uno dei fattori che hanno rallentato la diffusione dei linguaggi dichiarativi come linguaggi di programmazione general-purpose è l'assenza di strumenti adeguati per lo sviluppo (ambienti visuali, debugger,...). In particolare per il caso dei linguaggi funzionali e logico-funzionali, lo sviluppo di tecniche di debugging risulta particolarmente complesso quando si considerano strategie di valutazione. Task UD3.1 Un primo obiettivo di questo task è fornire un framework per la diagnosi automatica di codice funzionale e logico funzionale, ossia un metodo che, dato un programma (funzionale, logico-funzionale), sia in grado di riconoscere la presenza di errori nel codice rispetto ad una (descrizione implicita o esplicita) della semantica del programma (e rispetto ad una data strategia di valutazione). Si affronterà il problema della diagnosi seguendo l'approssimazione conosciuta come abstract diagnosis [CLMV97,Com98],CominiLMV96,CominiLV95, la quale fa largo uso di tecniche di interpretazione astratta e permette il riconoscimento di errori in una classe piuttosto ampia di programmi senza che l'utente debba determinare a priori possibili sintomi di malfunzionamento. L'Abstract Diagnosis è un framework per il debugging ottenuto estendendo con le metodologie dell'Int. Astr. la diagnosi dichirativa, permettendo di considerare (in modo parametrico) una qualsiasi proprietà astratta anziché la sola semantica denotazionale. Gode inoltre della flessibilità delle tassonomie di astrazioni che facilmente si definiscono in Int. Astr.. In particolare è stata definita una metodologia di debugging, come semplice arricchimento della teoria base, mediante la quale rendere il debugging – nel caso di proprietà astratte che producono specifiche astratte finite – effettivo. Il guadagno di effettività va a scapito della precisione, ma sono stati mostrati alcuni semplici esempi di come all'atto pratico si ottengono importantissimi riscontri (come mostrato dalle metodologie di diagnosi ottenute: Partial diagnosis, Diagnosis w.r.t. approximate properties, Modular diagnosis). Abbiamo realizzato vari prototipi di strumenti di diagnosi implementando gli algoritmi di diagnosi su alcuni domini tipici. Poiché i componenti fondamentali della metodologia sono Interpretazioni Astratte, che sono indipendenti dal linguaggio, ci aspettiamo di poter "scalare" la tecnica appunto a linguaggi funzionali e logico-funzionali scegliendo opportunamente una semantica concreta adatta. TASK UD3.2 Vogliamo inoltre definire un metodo per la correzione automatica di programmi funzionali e logico-funzionali, che permetta di riparare gli eventuali malfunzionamenti riconosciuti durante la fase di diagnosi. A tal fine si impiegheranno tecniche di machine learning per la sintesi di codice dichiarativo. La ricerca di una regola corretta durante il processo di sintesi può realizzarsi in modo top-down (ossia, partendo da regole molto specifiche e ottenendo regole di volta in volta più generali), oppure in modo bottom-up (ossia, raffinando regole generali al fine di conseguire regole via via più specifiche). In generale, è preferibile l'impiego di metodologie top-down in quanto riducono considerevolmente lo spazio di ricerca. Sfortunatamente, le metodologie top-down permettono di inferire correzioni rispetto a una classe di programmi piuttosto ristretta. Le metodologie bottom-up, più costose in quanto a tempo di esecuzione, hanno invece una maggior capacità di correzione. Il gruppo di Udine intende sviluppare un metodo di sintesi ibrido, che combini le due metodologie, allo scopo di riparare una classe più ampia di programmi funzionali, logico-funzionali e con vincoli in maniera effettiva ed efficiente. TASK UD3.3 Un altro obiettivo di questo task è quello di utilizzare un framework generale che abbiamo definito per il debugging di programmi logici che è parametrico rispetto a una proprietà del comportamento concreto del programma (purché quest'ultima sia esprimibile come una interpretazione astratta). Vogliamo generalizzare questa tecnica ai linguaggi con vincoli che sono usati in questo progetto per la specifica di sistemi reattivi e controllare i vantaggi che dà su casi forniti dall'industria. Ciò consentirebbe di verificare formalmente, per esempio, che il codice non produce overflow a tempo di esecuzione o, nel caso la verifica automatica fallisca, per identificare i punti del programma che devono essere modificati con un controllo a runtime dell'overflow. TASK UD3.4 Seguendo il programma presentato in questo workpackage (WP3) svilupperemo un prototipo di implementazione del debugger e correttore per linguaggi con vincoli. Implementeremo pure un model checker che operi su constraints, come descritto nel workpackage WP5. WP4: Sistemi ibridi e real-time Task UD4.1 L'utilizzo di linguaggi temporizzati basati sulla manipolazione dei vincoli come il tcc (timed concurrent constraint) [BGM95,SJG94b,SJG95,BGM00,PV01] consente di specificare in maniera naturale un sistema attraverso l'insieme dei vincoli che esso soddisfa in un dato istante. Questa disciplina di programmazione consente di modellare in maniera naturale anche aspetti concernenti la coordinazione di risorse. Dal lato della verifica, i linguaggi temporizzati con vincoli come quelli menzionati sopra hanno generalmente il problema che il modello generato ha un insieme di stati infinito. Questo problema e` stato affrontato e studiato in [FPV00,FPV01] con una proposta consistente nel limitare l'intervallo di tempo per il quale la verifica ha luogo. Ciò è realizzato fornendo automaticamente una riduzione finita e sufficientemente espressiva dell'universo degli stati. Ora abbiamo in programma di implementare un model checker che usa questa tecnica, o come un prodotto a se stante, o come un compilatore da linguaggi temporizzati con vincoli a strutture di Kripke, che possano in seguito essere date in input a model checker più noti, quale ad esempio Spin. Stiamo anche sviluppando metodologie basate sulla interpretazione astratta [CC92] per ridurre lo spazio degli stati per i modelli generati da questo tipo di linguaggi, e pertanto verificare i programmi senza la necessita` di scegliere un intervallo di tempo. L'implementazione del nostro model checker sarà successivamente estesa con queste caratteristiche. Task UD4.2 In alternativa, esploreremo la possibilità di utilizzare strumenti formali alternativi per la specifica e la verifica di sistemi basati sulla combinazione di logiche/automi [FM03,FM04,FMR04]. Le soluzioni ottenute tramite metodologie, tecniche e strumenti basati su formalismi logici e automi verranno quindi confrontate in modo sistematico con quelle basate sull'utilizzo dell'interpretazione astratta. Particolare attenzione verrà riservata ad una classe rilevante di sistemi reattivi le cui componenti evolvono su scale temporali diverse (si consideri, ad esempio, il sistema di controllo di un impianto idroelettrico) o le cui proprietà vanno specificate rispetto ad un insieme finito o infinito di granularità temporali diverse (non separabilità temporale di stati distinti del sistema, fenomeni di crescita/decadimento esponenziale, etc.) [EM04]. WP5: Constraints Nel paradigma della programmazione concorrente con vincoli (CC) si incontrano vari linguaggi temporali dove la nozione del tempo permette di modellare tanto sistemi ibridi quanto sistemi real-time in una forma molto intuitiva. Detti linguaggi non forniscono alcuna proprietà con la cui ottenere algoritmi di verifica effettivi. Task UD5.1 Partiremo da un modello dei sistemi reattivi che utilizza il linguaggio TCCP, analizzando le sue proprietà e paragonandolo con altri paradigmi. Estenderemo i lavori di verifica in [FPV00,FV03] studiando nuovi algoritmi di model checking più efficienti e capaci di gestire sistemi più complessi (con un numero di stati più elevato o persino infinito). In primo luogo, definiremo una struttura capace di rappresentare simbolicamente i vincoli usati nel nostro framework, così come gli algoritmi necessari per la costruzione e la manipolazione di tale struttura. La struttura permetterà di estendere quella presentata in [MLAH99] chiamata DDD, dato che tale struttura non permette di rappresentare tutti i vincoli presenti nei programmi tccp. A partire da questa struttura potremo definire un metodo di model checking simbolico che sarà implementato e che potremo quindi confrontare col metodo esaustivo, precedente, rispetto al quale prevediamo un notevole miglioramento della velocità di esecuzione. Task UD5.2 Inoltre lavoreremo sulla definizione di astrazioni di sistemi di vincoli che permettano di definire metodi astratti di model-checking. I metodi astratti permettono di avere metodologie per trattare sistemi definiti su variabili con dominio infinito (che generano sistemi con un numero infinito di stati). WP6: Verifica automatica Task UD6.1 Esistono in letteratura molto proposte per la verifica di Linguaggi Logici e Linguaggi Funzionali. In [CGLV03,CGL01a,CGL01b] abbiamo introdotto l'Abstract Verification Framework, un framework per la verifica di Linguaggi Logici ottenuto applicando le metodologie dell'Int. Astr. alle metodologie basate sulla semantica. Tale framework serve sia per l'organizzazione che per la sintesi di metodi di verifica per programmi logici parametrici rispetto ad una proprietà astratta d'interesse. Questo framework è in grado sia di ricostruire metodi ben noti in letteratura che di guidare nello sviluppo di strumenti nuovi. Questa metodologia di approccio alla Verifica, essendo basato su Int. Astr. che è indipendente dal linguaggio, può essere generalizzato ad altri paradigmi. Intendiamo procedere ad estendere questa metodologia alla classe dei linguaggi funzionali e logico-funzionali, con la contestuale produzione di nuovi tool di verifica per questo paradigma. Un inizio di tale lavoro si può trovare in [ACE+03] dove abbiamo ottenuto un prototipo di framework per il debugging astratto di programmi funzionali modellati come term rewriting systems. Ci aspettiamo che dei risultati molto utili possono venire dalla combinazione di domini usati per l'analisi con domini che modellano linguaggi di asserzioni (tipici della verifica tradizionale). Domini di questo genere possono perdere di completezza rispetto a quelli più tradizionali ma risultano effettivi, e possono quindi essere usati all'interno di nuovi strumenti di supporto alla programmazione di applicazioni complesse. Data la struttura parametrica con cui è stato scritto il codice degli strumenti già realizzati i nuovi prototipi si potranno ottenere semplicemente re-implementando solo le operazioni canoniche dei nuovi domini. Task UD6.2 Per quanto riguarda gli ambienti per la specifica e la verifica di sistemi reattivi caratterizzati da strutture temporali multi-livello, verranno prese in esame alcune delle principali soluzioni, basate su formalismi logici e automi, proposte in letteratura, comprendenti le logiche temporali lineari estese con vincoli di periodicità su interi [Dem03], le logiche temporali lineari estese con operatori stereo [MPP02], le estensioni delle teorie monadiche al primo e second'ordine di un successore e di k successori [MPP99], le logiche temporali metriche e stratificate [Mo96], le logiche temporalizzate [FM04]) e logiche temporali ad intervalli [MSV02], sul versante delle logiche, e gli automi single-string [DLM01], automi single-string estesi con contatori [DMP03], automi fondamentalmente periodici [BMP03], automi sistolici [MPP99], automi di Rabin su alberi con archi etichettati e nodi colorati [MP04], automi temporizzati [FM04], sul versante degli automi. Più in generale, negli ultimi anni sono stati proposti diversi approcci alla specifica e verifica di sistemi reattivi a stati infiniti basati sulla logica e sulla teoria degli automi che presentano interessanti punti di contatto con i formalismi di interesse per il presente progetto. L'unità di Udine intende investigare le potenzialità dell'interpretazione astratta attraverso un confronto sistematico con gli strumenti messi a disposizione da tali ambienti.
