22 12 10

Pagina 1

Dipartimento di Elettronica e Informazione Politecnico di Milano prof. Elisabetta Di Nitto, Carlo Ghezzi e Raffaela Mirandola 20133 Milano (Italia) Piazza Leonardo da Vinci, 32 Tel. (39) 02-2399.3400 Fax (39) 02-2399.3411 Ingegneria del Software II 22 Dicembre 2010 Cognome Nome Matricola Note 1. La mancanza dei dati di cui sopra comporta l'annullamento dell'esame 2. Restituire solo queste pagine. Verranno ignorati fogli aggiuntivi. Si puo' scrivere con la matita. 3. È proibito l'uso di dispositivi elettronici (computers, calcolatrici, cellulari, macchine fotografiche). 4. Non si puo' tenere una copia del testo dell'esame quando si lascia l'aula. 2 Domanda 1 – Alloy (8 punti) Una macchina a stati ha uno o più stati iniziali e una relazione di transizione che connette ciascuno stato ai suoi successori. (a) Si costruisca in Alloy un modello di macchina a stati. (b) Si aggiungano i vincoli per specificare i seguenti casi particolari: i. Macchine deterministiche, in cui ciascuno stato ha al più un successore; ii. Macchine non deterministiche, in cui gli stati possono avere più successori; iii. Macchine con stati irraggiungibili; iv. Macchine senza stati irraggiungibili; v. Una macchina connessa in cui ogni stato è raggiungibile da ogni altro stato; vi. Una macchina con deadlock: uno stato raggiungibile non ha successori; (c) Come si può visualizzare un esempio di macchina a stati con stati irraggiungibili? (d) Nel caso di macchine a stati deterministiche, come si può validare la specifica generando un contro esempio che mostri che uno stato non può avere più di un successore? (e) Si definiscano i fatti che modellano una macchina con livelock: possibilità di avere un’esecuzione infinita in cui uno stato che è sempre raggiungibile non è mai raggiunto. Soluzione (a) sig…