BEGIN:VCALENDAR PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN CALSCALE:GREGORIAN X-WR-CALNAME:Calagator METHOD:PUBLISH VERSION:2.0 BEGIN:VTIMEZONE TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles BEGIN:STANDARD DTSTART:20101107T020000 RDATE:20101107T020000 TZOFFSETFROM:-0700 TZOFFSETTO:-0800 TZNAME:PST END:STANDARD END:VTIMEZONE BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20101109T220517Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101116T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20101116T103000 DTSTAMP;VALUE=DATE-TIME:20101109T220517Z LAST-MODIFIED;VALUE=DATE-TIME:20101109T220517Z UID:http://calagator.org/events/1250459459 DESCRIPTION:speaker: Alwyn Goodloe \;\n \;\nCritical 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 foundat ions\, but control engineers typically only work on Matlab/Simulink mode ls\, ignoring the implementation all together. I will speak about an ong oing collaboration with Prof. Eric Feron of Georgia Tech aimed at narrow ing this gap. I will briefly describe the design of a Matlab to C transl ator being written in Haskell and verified using the Frama-C tool and th e Prototype Verification System (PVS). In addition\, I will give a surve y of our efforts in enhancing PVS’ capabilities in this area by building a Linear Algebra library targeted at the math used by control engineers .\n\nTags: galois\, tech talk\, control systems\, formal methods\n\nImpo rted from: http://calagator.org/events/1250459459 URL:http://www.galois.com/blog/2010/11/09/tech-talk-formal-methods-applie d-to-control-software/ SUMMARY:Galois Tech talk: Formal Methods Applied to Control Software LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT END:VCALENDAR