Formal Methods

Competency Leader

Research at Lero@TCD into Formal Methods

The Foundations and Methods Group (FMG) at TCD has been actively involved in formal methods research from its inception in 1992, and has recently started collaborative work with Lero with both the Foundations for Software Engineering (FSE) and Autonomic Software Systems (AUS) strands.

This work has been led byDr Andrew Butterfield, Head of FMG. The focus of his recent research work has been exploring the application of formal reasoning techniques to the boundary between hardware and software.

Dr Butterfield’s recent work has looked at providing formal semantics to cover real-world hardware compilation languages, in order to be able to support formal reasoning for users of those languages. In particular he has published on the semantics of Handel-C, a commercial hardware compiler, with an emphasis on covering the difficult aspects of that language, rather than restricting attention to simple subsets (BW 2005, Butterfield 2007). He also got involved in a pilot project to develop a ‘top-to-toe’ formal model of a POSIX filestore implemented on top of flash memory, as part of the international grand challenge project called the Verified Software Initiative. His focus was at the ‘toe’, developing formal models of the flash memory devices at the hardware level (BFW 2008, BO 2009). During this time, he adopted the so-called “Unifying Theories of Programming” (UTP) paradigm as a basis for his foundational work, and has developed generic theories of programming languages suited for modelling synchronously clocked hardware (BSW 2007, ), and is currently exploring linkages to other related languages, as well as exploring probabilistic aspects in a unifying setting. As part of this work, an experimental theorem-prover has also been developed, to support UTP (Butterfield 2010). The UTP and grand challenge work has been supported by Science Foundation Ireland since September 2007.

Dr Butterfield is actively involved on the program committees of various conferences, and has been program (co-)chair for several: IFL 2005, FMICS 2004, UTP 2008, as well as being an active review for a number of journals (FAC-J, Software Informatics, Concurrency and Computation: Practice and Experience, IEEE Computer, IEEE TSE).

The collaboration with Lero group has mainly been focusing on planning the exploration of formal techniques for reasoning about the specification and development of autonomic systems, with a particular emphasis on modelling the physical environment of such systems. Also Dr Butterfield’s research team has actively participated in Lero Research workshops in recent years.

We have also hosted a series of occasional Friday afternoon talks on formal methods and foundations as a vehicle to encourage the exchange of results and ideas between the various researchers in the various Lero institutions.

Bibliography (cited)

(BW 2005) Butterfield, A. & Woodcock, J. “prialt in Handel-C: an operational semantics” International Journal on Software Tool for Technology Transfer (STTT), Springer, 2005.

(Butterfield 2007) Butterfield, A. “A Denotational Semantics for Handel-C” in Jones, C. B.; Liu, Z. & Woodcock, J. (ed.) Formal Methods and Hybrid Real-Time Systems, Springer, 2007, 4700, 45-66.

(BSW 2007) Butterfield, A.; Sherif, A. & Woodcock, J. “Slotted-Circus: A UTP-Family of Reactive Theories” in Davies, J. & Gibbons, J. (eds.) Integrated Formal Methods, Springer, 2007, 4591, 75-97

(BFW 2008) Butterfield, A.; Freitas, L. & Woodcock, J. “Mechanising a formal model of flash memory” in Science of Computer Programming, 2009, 74, 219 – 237.

(BO 2009) Butterfield, A. & O’Catháin, A. “Concurrent Models of Flash Memory Device Behaviour” in Woodcock, J. & Oliveira, M. (eds.) 12th Brazilian Symposium on Formal Methods, SBMF 2009, Springer, 2009, 5902, 70-83.

(GB 2010) Gancarski, P. & Butterfield, A. “Prioritized slotted-Circus”, in Déharbe, D. & Cavalcanti, A. (eds.) 7th International Colloqium on Theoretical Aspects of Computing, ICTAC 2010, Springer, 2010, to appear, 16p.

(Butterfield 2010) Butterfield, A. Saoithin: “A Theorem Prover for UTP” in Qin, S. (ed.) Unifying Theories of Programming, Third International Symposium, UTP 2010, Shanghai, China, November, 2010., Springer, 2010, accepted, to appear, 20p.

Bibliography (recent, not cited abov, incomplete ):

(Butterfield 2010b) Butterfield, A. (ed.) Unifying Theories of Programming, Second International Symposium, UTP 2008, Dublin, Ireland, September, 2008, Revised Selected Papers, Springer, 2010, 5713

(Butterfield 2010a) Butterfield, A. “A Denotational Semantics for Handel-C” Formal Aspects of Computing, 2010, Online First.

(BFW 2009) Butterfield, A.; Freitas, L. & Woodcock, J. “Mechanising a formal model of flash memory” in Science of Computer Programming, 2009, 74, 219 – 237.

(GBW 2009) Butterfield, A.; Gancarski, P. & Woodcock, J. “State Visibility and Communication in Unifying Theories of Programming” in Chin, W. & Qin, S. (eds.) 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, Tianjin, China, July 29-31, IEEE Computer Society, 2009, 47-54.

(GB 2009) Gancarski, P. & Butterfield, A. “The Denotational Semantics of slotted-Circus” in Cavalcanti, A. & Dams, D. (eds.) FM2009: Formal Methods, Springer, 2009, 5850, 451-466.

(BBA 2007) Butterfield, A.; Bicarregui, J. & Arenas, A. (eds.) “Foreword: Selected papers from the ninth international workshop on formal methods for industrial critical systems (FMICS 04), Linz, Austria”, Formal Methods in System Design, 2007, 30, 177-178

(BGH 2006) Butterfield, A.; Grelck, C. & Huch, F. (ed.) Implementation and Application of Functional Languages, 17th International Workshop, IFL 2005, Dublin, Ireland, September 19-21, 2005, Revised Selected Papers Springer, 2006, 4015.