You are here

Publications

  1. Alessandro Cimatti; Fausto Giunchiglia; G. Mongardi; D. Romano; F. Torielli; Paolo Traverso,
    in «FORMAL ASPECTS OF COMPUTING»,
    1998
    , pp. 361 -
    380
  2. Alessandro Cimatti; E.M. Clarke; Fausto Giunchiglia; Marco Roveri,
    NuSMV: A Reimplementation of SMV,
    International Workshop on Software Tools for Technology Transfer (STTT-98),
    vol.NS-98-4,
    1998
    , pp. 25-
    31
    , (International Workshop on Software Tools for Technology Transfer (STTT-98),
    1998)
  3. Alessandro Cimatti; Marco Roveri; Paolo Traverso,
    Fourth International Conference on Artificial Intelligence Planning Systems [AIPS-98],
    1998
    , (Fourth International Conference on Artificial Intelligence Planning Systems [AIPS-98],
    Pittsburgh, USA,
    1998)
  4. Alessandro Cimatti; Marco Roveri; Paolo Traverso,
    Automatic OBDD-based Generation of Universal Plans in Non-Deterministic Domains,
    Fifteenth National Conference on Artificial Intelligence [AAAI 98],
    AAAI Press,
    1998
    , pp. 875-
    881
    , (Fifteenth National Conference on Artificial Intelligence [AAAI 98],
    Madison, USA,
    1998)
  5. Piergiorgio Bertoli; Alessandro Cimatti; Fausto Giunchiglia; Paolo Traverso,
    A Structured Approach to the Formal Certification of Safety of Computer Aided Development Tools,
    17th International Conference on Computer Safety, Reliability and Security [SAFECOMP ‘98],
    Springer,
    vol.1516,
    1998
    , pp. 221-
    230
    , (17th International Conference on Computer Safety, Reliability and Security [SAFECOMP ‘98],
    Heidelberg, Germany,
    1998)
  6. Alessandro Cimatti; Fausto Giunchiglia; Marco Roveri,
    Abstraction in Planning via Model Checking,
    Symposium on Abstraction, Reformulation and Approximation (SARA 1998),
    1998
    , pp. 37-
    41
    , (Symposium on Abstraction, Reformulation and Approximation (SARA 1998),
    1998)
  7. Alessandro Cimatti; Fausto Giunchiglia; G. Mongardi; D. Romano; F. Torielli; Paolo Traverso,
    Model Checking Safety Critical Software with SPIN: An Application to a Railway Interlocking System,
    17th International Conference on Computer Safety, Reliability and Security [SAFECOMP ‘98],
    Springer,
    vol.1516,
    1998
    , pp. 284-
    295
    , (17th International Conference on Computer Safety, Reliability and Security [SAFECOMP ‘98],
    Heidelberg, Germany,
    1998)
  8. Alessandro Cimatti; Roberto Sebastiani,
    Servizi forniti dagli strati Safety Layer e Connection Manager,
    Obiettivo del presente documento è fornire una (proposta preliminare di) descrizione dei servizi forniti agli applicativi dagli strati Connection Manager (CM) e Safety Layer (SL), come perzialmente descritto nei documenti (1) e (3). Tale proposta è risultante della riunione in Ansaldo del 08-05-98 tra Ansaldo e Irst,
    1998
  9. Alessandro Cimatti; Roberto Sebastiani,
    Specifica formale dei protocolli Safety Layer e Connection Manager,
    Il presente documento descrive una specifica formale del protocollo di comunicazione tra applicativi in sicurezza basato su ridondanza. Il protocollo è stato suddiviso in due livelli separati, il Safety Layer (SL), come parzialmente descritto nei documenti (1) e (3), ed il Connection Manager (CM). Il S: e il CM sono stati specificati formalmente in SDL, e sono state applicate tecniche di validazione basate su simulazione esaustiva (model checking) attraverso il tool ObjectGEODE Nel presente documento vengono descritti i servizi forniti da tali livelli, e viene descritta la specifica formale delle macchine a stati che realizzano i livelli CM e SL. i dettagli del codice SDL sono descritti nel documento (6).,
    1998
  10. Alessandro Cimatti; Roberto Sebastiani,
    Protocolli Safety Layer e Connection Manager: Descrizione del Codice SDL,
    Nel presente documento viene descritto in dettaglio il codice SDL della specifica formale dei protocolli Safety Layer (SL) e Connection Manager (CM) descritta in (1). Il modello è realizzato attraverso i meccanismi di 'definizione di tipo' e di 'istanziazione' di SDL. Il codice è ripartito nei fine terminale_lib.pr, contenente la descrizione dei tipi (es. macchina SL, macchina CM), e Modello.pr, contentenente le istanze che realizzano la particolare configurazione analizzata Il presente documento assume che il lettore abbia una certa conoscenza di SDL, e fa esplicito riferimento al listato dei file Modello.pr e terminale_lib.pr allegato.,
    1998

Pages