Proposte

Un nuovo set di progetti è disponibile (in costruzione), principalmente rivolto allo studio e sperimentazione di strumenti e tecniche volte alla predicibilità e al controllo del funzionamento di sistemi ICT complessi (altri sono disponibili, si senta col docente a ricevimento):

  • *groove - assigned to Cilotti*: Il tool Groove è uno strumento di model-checking per "graph transformation systems" e può essere utilizzato per modellare algoritmi su reti. Scopo del progetto è quello di sperimentare le sue funzionalità e di applicare a casi di studio (anche forniti dal docente) nell'ambito ICT.
  • *Augur -- assigned to Cicora*: Il tool Augur è uno strumento di model-checking per "graph transformation systems" e può essere utilizzato per modellare algoritmi su reti mobili e a larghissima scala. Scopo del progetto è quello di sperimentare le sue funzionalità e di applicare a casi di studio (anche forniti dal docente) nell'ambito ICT.
  • *Spatial Fluid Flow approximation -- assigned to Mella*: Scopo del progetto è sperimentare l'applicabilità di una tecnica di analisi per algoritmi auto-organizzanti, che prevedere la costruzioni automatica di un sistema di "Equazioni differenziali alle derivate parziali" a partire da un transition system. Tali equazioni possono essere analizzate usando poi strumenti standard come matlab.
  • *alchemist-mc*: Alchemist è un simulatore per sistemi chimici scritto in Java nel nostro laboratorio. Il goal del progetto è quello di costruire un componente denominato "Revolver", in grado di pianificare set di simulazioni, dando luogo all'approccio dell'approximate stochastic model-checking.

I progetti precedentemente proposti sono tuttavia ancora validi:

  • *2p-libs*: (this is actually a project template) porting existing libraries of other Prologs (SWI, GNU, SICSTUS) into tuProlog; generally, even libraries for Java could be used
  • *2p-imperative-language*: The various step of a full interpreter (tokenization, parsing, checking and interpretation) can be specified declaratively, using BNF grammars and deductions. This projects will implement in tuProlog suitable meta-interpreters for those specifications, by adding proper (infix/prefix) operators and syntactic sugar.
  • *maude-2p*: Prolog and Maude can interact with each other, e.g. by sockets; this project should develop flexible libraries for both sides of the integration
  • *maude-compmodels*: This project aims at programming in Maude the syntax/semantics of some computational model, possibly adding model-checking abilities. Examples can include: FJ, SAPERE model, advanced petri net models, process algebras.
  • *models-mu*: The mu-calculus is a temporal logic that is shown to be more expressive than CTL, and to also have a reasonably simple to define model-checking algorithm. This project aims at surveying the basic concepts of mu-calculus, and evaluate the possibility of implementing its model-checking in tuProlog or Maude.