Le notazioni diagrammatiche sono usate estensivamente in pressoché ogni disciplina scientifica e tecnica, come pure nella pratica quotidiana in molte aree di comunicazione. In modo particolare, la moderna ingegneria del software usa comunemente notazioni diagrammatiche: UML sta rapidamente divenendo la lingua franca per l’ingegneria del software. Sfortunatamente, mentre le semantiche astratte sottostanti alle varie notazioni diagrammatiche sono solitamente ben formalizzate, le notazioni in sé raramente lo sono. Questo impedisce una corretta formalizzazione di processi di ingegneria del software mediante notazioni diagrammatiche. Per esempio, senza una corretta formalizzazione dei diagrammi UML non è possibile basare direttamente sulla notazione processi fondamentali dell’ingegneria del software, quali il raffinamento e il controllo di coerenza. Di conseguenza, lo sviluppo di calcoli per la formalizzazione di notazioni diagrammatiche e il loro uso in processi di ragionamento sta divenendo un'area di ricerca molto attiva. Lo scopo della visita proposta è estendere il recente lavoro, intrapreso congiuntamente con l'Università di Roma su formalismi di specifica basati su logica lineare per notazioni diagrammatiche statiche, alla specifica del comportamento dinamico del diagramma in modo da rendere questi formalismi completamente adeguati per la specifica di tali notazioni. I formalismi per il ragionamento basato su diagrammi devono affrontare tre problemi: principali: (1) modellazione adeguata della sintassi spaziale, (2) definizione di strumenti per la modifica dinamica dei diagrammi, e (3) definizione di metodi adatti per il ragionamento automatizzato. Praticamente tutti i formalismi esistenti sono basati o su tecniche di riscrittura o su specifiche logiche. Le tecniche di riscrittura hanno di solito successo nel trattare i problemi (1) e (2), mentre le specifiche basate sulla logica affrontano con successo il problema di ragionare coi diagrammi, ma hanno in genere difficoltà nel trattare il problema complementare della modifica dinamica: la logica classica del primo ordine riesce difficilmente a gestire il tipo di cambiamento non monotono qui richiesto. In un lavoro congiunto con P. Bottoni e F. Parisi Presicce dell‘Università di Roma abbiamo recentemente mostrato come la specifica di notazioni diagrammatiche, ed in particolare il parsing di diagrammi può essere ambientato in un quadro di logica lineare. A nostra conoscenza, questo è la prima codifica logica, basata su predicati, della sintassi di diagrammi che possa modellare il processo di parsing in modo assolutamente fedele Ancora più importante è il fatto che la logica lineare, che è alla base del nostro approccio, è accompagnata da un calcolo deduttivo di risorse ed azioni che sussume completamente la logica classica del primo ordine e che modella cambiamenti non monotoni. Il nostro approccio supera perciò anche i problemi che sorgono dalla monotonicità della logica classica del primo ordine e ci fornisce in modo effettivo il fondamento per un calcolo deduttivo, per la sintassi e la semantica di diagrammi, che possa modellare il ragionamento mediante manipolazione di diagrammi, come richiesto, per esempio, dal ragionamento con diagrammi UML. Il proponente e il candidato hanno compiuto degli studi pilota in questa area. Questi lavori possono essere visti come preliminari e ci si ripromette di estenderli durante la visita proposta. In particolare andrà rivisitata la modellazione delle relazioni spaziali per permettere una manipolazione dinamica coerente. Ci si propone di utilizzare il calcolo riveduto per formalizzare una parte significativa del linguaggio dei “Constraint Diagrams”, una estensione proposta di UML, intesa come un sostituto /complemento di OCL. Nel medio termine, si intende usare un interprete per il nostro calcolo dei diagrammi, attualmente sotto implementazione in un lavoro congiunto con A. Sterbini, pure del Dipartimento di Scienze dell’Informazione a “La Sapienza”, allo scopo di catturare adeguatamente il trattamento dinamico di vincoli spaziali e di usare questo interprete rivisitato per l’implementazione del linguaggio dei “Constraint Diagrams”.
Formalizzazione di Notazioni Diagrammatiche dell’Ingegneria del Software in un Approccio Basato su Logica Lineare / Bottoni, Paolo Gaspare; Bernd, Meyer. - (2003).
Formalizzazione di Notazioni Diagrammatiche dell’Ingegneria del Software in un Approccio Basato su Logica Lineare
BOTTONI, Paolo Gaspare;
2003
Abstract
Le notazioni diagrammatiche sono usate estensivamente in pressoché ogni disciplina scientifica e tecnica, come pure nella pratica quotidiana in molte aree di comunicazione. In modo particolare, la moderna ingegneria del software usa comunemente notazioni diagrammatiche: UML sta rapidamente divenendo la lingua franca per l’ingegneria del software. Sfortunatamente, mentre le semantiche astratte sottostanti alle varie notazioni diagrammatiche sono solitamente ben formalizzate, le notazioni in sé raramente lo sono. Questo impedisce una corretta formalizzazione di processi di ingegneria del software mediante notazioni diagrammatiche. Per esempio, senza una corretta formalizzazione dei diagrammi UML non è possibile basare direttamente sulla notazione processi fondamentali dell’ingegneria del software, quali il raffinamento e il controllo di coerenza. Di conseguenza, lo sviluppo di calcoli per la formalizzazione di notazioni diagrammatiche e il loro uso in processi di ragionamento sta divenendo un'area di ricerca molto attiva. Lo scopo della visita proposta è estendere il recente lavoro, intrapreso congiuntamente con l'Università di Roma su formalismi di specifica basati su logica lineare per notazioni diagrammatiche statiche, alla specifica del comportamento dinamico del diagramma in modo da rendere questi formalismi completamente adeguati per la specifica di tali notazioni. I formalismi per il ragionamento basato su diagrammi devono affrontare tre problemi: principali: (1) modellazione adeguata della sintassi spaziale, (2) definizione di strumenti per la modifica dinamica dei diagrammi, e (3) definizione di metodi adatti per il ragionamento automatizzato. Praticamente tutti i formalismi esistenti sono basati o su tecniche di riscrittura o su specifiche logiche. Le tecniche di riscrittura hanno di solito successo nel trattare i problemi (1) e (2), mentre le specifiche basate sulla logica affrontano con successo il problema di ragionare coi diagrammi, ma hanno in genere difficoltà nel trattare il problema complementare della modifica dinamica: la logica classica del primo ordine riesce difficilmente a gestire il tipo di cambiamento non monotono qui richiesto. In un lavoro congiunto con P. Bottoni e F. Parisi Presicce dell‘Università di Roma abbiamo recentemente mostrato come la specifica di notazioni diagrammatiche, ed in particolare il parsing di diagrammi può essere ambientato in un quadro di logica lineare. A nostra conoscenza, questo è la prima codifica logica, basata su predicati, della sintassi di diagrammi che possa modellare il processo di parsing in modo assolutamente fedele Ancora più importante è il fatto che la logica lineare, che è alla base del nostro approccio, è accompagnata da un calcolo deduttivo di risorse ed azioni che sussume completamente la logica classica del primo ordine e che modella cambiamenti non monotoni. Il nostro approccio supera perciò anche i problemi che sorgono dalla monotonicità della logica classica del primo ordine e ci fornisce in modo effettivo il fondamento per un calcolo deduttivo, per la sintassi e la semantica di diagrammi, che possa modellare il ragionamento mediante manipolazione di diagrammi, come richiesto, per esempio, dal ragionamento con diagrammi UML. Il proponente e il candidato hanno compiuto degli studi pilota in questa area. Questi lavori possono essere visti come preliminari e ci si ripromette di estenderli durante la visita proposta. In particolare andrà rivisitata la modellazione delle relazioni spaziali per permettere una manipolazione dinamica coerente. Ci si propone di utilizzare il calcolo riveduto per formalizzare una parte significativa del linguaggio dei “Constraint Diagrams”, una estensione proposta di UML, intesa come un sostituto /complemento di OCL. Nel medio termine, si intende usare un interprete per il nostro calcolo dei diagrammi, attualmente sotto implementazione in un lavoro congiunto con A. Sterbini, pure del Dipartimento di Scienze dell’Informazione a “La Sapienza”, allo scopo di catturare adeguatamente il trattamento dinamico di vincoli spaziali e di usare questo interprete rivisitato per l’implementazione del linguaggio dei “Constraint Diagrams”.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
