Formal Methods Seminar News
Seminar on Friday, April 13, 2012 - Using non-convex abstractions for efficient analysis of timed automata
Blog post added by Edgar Pek
Title: Using non-convex abstractions for efficient analysis of timed automata.
Speaker: Dileep Kini, UIUC
Venue: 3401 SC
Time: 3:00pm-4:00pm, Friday, April 13, 2012
We consider the classic reachability problem for timed automata: given an automaton, decide if there exists a path from its initial state to a given target state. The standard solution to this problem involves computing the zone graph of the automaton, which in principle could be infinite. In order to make the graph finite, zones are approximated using an extrapolation operator. For reasons of efficiency it is required that an extrapolation of a zone is always a zone; and in particular that it is convex. We propose a new solution to the reachability problem that uses no such extrapolation operators. To ensure termination, we provide an efficient algorithm to check if a zone is included in the region closure of another. Although theoretically better, closure cannot be used in the standard algorithm since a closure of a zone may not be convex. The structure of this new algorithm permits to calculate approximating parameters on-the-fly during exploration of the zone graph, as opposed to the current methods which do it by a static analysis of the automaton prior to the exploration. This allows for further improvements in the algorithm.View Online Edgar Pek 2012-04-12T19:44:35Z
Blog post edited by Edgar Pek
Title: Foundations of Verification with Proof Scores in CafeOBJ
Speaker: Kokichi Futatsugi (JAIST, Japan)
Venue: 3405 SC
Time: 2:00pm-3:15pm, Tuesday, April 10, 2012
The verification method with proof scores is an interactive theorem proving method based on algebraic specifications. We have been developing verifications with proof scores in CafeOBJ algebraic specification language for more than ten years. This talk explains theoretical foundations of verification with proof scores using simple and insightful examples. The focuses of the talk are (1) model based verification, (2) quasi-complete proof rules, (3) analysis of relations between specifications and proofs.
Kokichi Futatsugi is a professor at Graduate School of Information Science, JAIST (Japan Advanced Institute of Science and Technology). His primary research goal is to design and develop new computer languages which can open up new application areas, and/or improve the current software technology. His current approach for this goal is CafeOBJ formal specification language. CafeOBJ is multi-paradigm formal specification language which is a modern successor of the most noted algebraic specification language OBJ. CafeOBJ adopts hidden algebra and rewriting logic as its underlying logics and its application areas include design and validation of fundamental and important systems such as component based systems, security/safety systems, computer language systems, etc. Some parts of research around CafeOBJ are being conducted in cooperation with IPA (Information-Technology Promotion Agency, Tokyo, Japan), SRI (California, USA), Univ. of California at San Diego (USA), and Univ. of Munich (Germany), ETL (Electrotechnical Lab.,Tsukuba, Japan), and several other companies and universities in Japan.View Online Edgar Pek 2012-04-06T17:22:00Z