• BPEL
• NetWeaver
• portal
• PVS
• SAP

In questa tesi è stato analizzato il modulo NetWeaver Portal della piattaforma NetWeaver di SAP AG per l'accesso integrato al sistema informativo aziendale ed è stato implementato un semplice portale pubblico accessibile via Internet basandosi su una realtà esistente.
Parallelamente alla definizione delle funzionalità fornite dal portale, è importante definire anche i processi di business ad esso collegati. Partendo da tali definizioni è infatti possibile analizzarne la correttezza ed eventuali ottimizzazioni.
Per tale scopo è stata esaminata la possibilità di simulazione ed analisi formale dei processi definiti all'interno di tale piattaforma NetWeaver.
E' stato implementato un simulatore semplificato di processi descritti mediante il linguaggio BPEL, utilizzando il sistema di specifica e verifica formale PVS.