Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!
- title:
- Formal Methods Applied to Control Software
- speaker:
- Alwyn Goodloe
- time:
- 10:30am, Tuesday, 16 November 2010
- location:
- Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
- abstract:
- Critical cyber-physical systems, such as avionics, typically have one or more components that control the behavior of dynamical physical systems. The design of such control systems is well understood with mature and sophisticated foundations, but control engineers typically only work on Matlab/Simulink models, ignoring the implementation all together. I will speak about an ongoing collaboration with Prof. Eric Feron of Georgia Tech aimed at narrowing this gap. I will briefly describe the design of a Matlab to C translator being written in Haskell and verified using the Frama-C tool and the Prototype Verification System (PVS). In addition, I will give a survey of our efforts in enhancing PVS’ capabilities in this area by building a Linear Algebra library targeted at the math used by control engineers.
- bio:
- Alwyn Goodloe obtained his B.Sc. in Computer Science from Old Dominion University in 1985 and an M.Sc. in Mathematics from George Mason University in 1992. He worked for fourteen years in the software industry as a software engineer, database administrator, Unix system administrator, and technologist. In 1999, he returned to graduate school to study at the University of Pennsylvania, where he obtained a Ph.D. in Computer and Information Science in 2008. At Penn he conducted research in the area of computer and network security. He is currently a research scientist at the National Institute of Aerospace in Hampton, Virginia. At NIA his research focus has been formal methods applied to high-reliable systems such as avionics.