Workshop on Formal Method and Internet of Mobile Things (FMIMT)
发布时间：2014-11-26 浏览量：5416
Shanghai, Nov. 27th-28th, 2014
FMIMT 2014
Workshop information
| Date: | Nov. 27th (Thurs.), 28th (Fri.), 2014 |
| Venue: | Room 201, Math Building, SEI, ECNU |
| Organizer: | Yixiang Chen (East China Normal University) |
Program
Opening (9:00 -- 9:10), Thurs., Nov. 27th
Session 1
9:10 -- 9:50, Speaker:
| Title: | |
| Abstract: | The state space of a transition system is defined as a quotient set (i.e. a set of equivalence classes) of terms of a top most sort State, and the transitions are defined with conditional rewrite rules over the quotient set. A property to be verified is either (1) an invariant (i.e. a state predicate that is valid for all reachable states) or (2) a (p leads-to q) property for two state predicates p and q. Where (p leads-to q) means that from any reachable state s with (p(s) = true) the system will get into a state t with (q(t) = true) no matter what transition sequence is taken. Verification is achieved by developing proof scores in CafeOBJ. Sufficient verification conditions are formalized for verifying invariants and (p leads-to q) properties. For each verification condition, a proof score is constructed to (1) generate a finite set of state patterns that covers all possible infinite states and (2) check validity of the verification condition for all the covering state patterns by reductions. |
9:50--10:30, Speaker:
| Title: | |
| Abstract: | We present a hybrid approach to improving the verification performance of SMT-based bounded model checking for LTL properties. In this approach, stateless explicit-state exploration is utilized to traverse, under the constraints of bounded context switches, the state space of a system design and memorize legal execution paths. These paths are classified according to certain predicates into path clusters, which are then encoded into propositional formulas representing independent BMC instances. Such BMC instances are solved with SMT solvers running on mutilcores in parallel. Once a counterexample is found for one of the instances, the entire model checking terminates. This hybrid checking procedure progresses in an incremental fashion until either a counterexample is found or the user-specified bound is reached. We have implemented this proposed hybrid approach in a tool called Garakabu2, which is to be demonstrated in this talk. |
Coffee break (10:30--10:40)
Session 2
10:40--11:20, Speaker:
| Title: | |
| Abstract: | This talk will cover "work in progress", our current attempt at doing some research that may or may not succeed. In this project, we try to generate a SystemC simulator of the ARM Version 7 Instruction Set starting from the only available source: the .pdf document from ARM company. I will explain first how we extracted an XML specification from the .pdf, so that we can get a formal processor specification. Next, from the specification, one wants to generate (i) a decoder to decode the binary instructions, which can be of variable size and (b) the SystemC/C++ code that can be directly compiled for the SimSoC simulator. I will explain briefly the C++ generation from XML and focus on the algorithm to generate the decoder, which raises decidability issues. |
11:20--12:00, Speaker:
| Title: | |
| Abstract: | A time-sensitive pushdown system is a framework for time-awareness program modeling and analysis. This talk begins with NeTAs, a time-sensitive pushdown system with only local clocks, discussing its decidability on reachability, and then gives a whole picture on the time-sensitive pushdown systems, revealing the decidability, undecidability, and unknown results, with reasonable conjectures. |
Lunch break (12:00 - 14:00)
Session 3
14:00--14:40, Speaker:
| Title: | |
| Abstract: | We demonstrate model checking designs with CafeOBJ, an algebraic specification language and system, through a contrast with model checking Java programs with Java Pathfinder (JPF), a software model checker. |
14:40--15:20, Speaker:
| Title: | |
| Abstract: | In this presentation, the speaker introduces the specification language for requirement of real-time systems with spatial-temporal consistency: STeC. After introducing the syntax of STeC, the speaker sets up its formal semantics including operational and denotational semantics. Then, the speaker shows the introduction of hybrid clock calculus which deals with both logic and chronomical clock. The santisfaction between STeC design and hybrid clock is estaibilshed. This presentation will show the tool related to STeC language. |
Coffee break (15:20--15:40)
Session 4
15:40--16:20, Speaker:
| Title: | |
| Abstract: | Timed-pNets is a semantic model to specify the communication behaviours of distributed systems. It has a tree style hierarchical structure. The leaves are timed specifications which consist of a set of logical clocks and clock relations. These logical clocks are encoded with delay variables and delay bound. In this presentation, we discuss how to detect time constraint conflicts and how to compute the delay variables of the clocks in the non-leaf nodes. Then we take a simple use case from ITS to simulate and check time properties. |
16:20--17:00, Speaker:
| Title: | |
| Abstract: | The OSEK/VDX is an international standard of automobile operating systems. Such systems are safety-critical and require extensive safety analysis and verification. Formal methods have been shown useful and effective to verify the safety of both the OSEK/VDX-based operating systems and applications. Using formal methods requires formal semantics of the OSEK/VDX standard. In this talk, we will present a formal semantics of the standard using K, a rewrite-based formal semantics framework. With the formal semantics, we can (1) verify user-defined applications by model checking, and (2) automatically generate test cases for testing of the OSEK/VDX-based operating systems. Features of the formal semantics are its executability and flexibility. Compared with ex- isting formal semantics of the standard, the formal semantics defined in K is more flexible and generic. This work also shows that K is not only used for formalizing the semantics of programming languages, but also for automobile operating systems. |
Participant
- Kokichi Futatsugi (JAIST)
- Kazuhiro Ogata (JAIST)
- Yixiang Chen (ECNU)
- Vania Joloboff (ECNU)
- Jianwen Xiang (WHUT)
- Chengming Zou (WHUT)
- Guoqiang Li (SJTU)
- Weiqiang Kong (DLUT)
- Min Zhang (ECNU)
- Yanwen Chen (ECNU)
- Xianqiao Chen (WHUT)
- Jianjun Chen (WHUT)
- Xing Tang (WHUT)
- Shengwu Xiong (WHUT)
Contact
| Min Zhang |
| Phone: +86 18521593581, +86 21 62232851 |
| Email: zhangmin(at)sei.ecnu.edu.cn |
快速通道:
