8th WAVAS

8th Workshop on Automated Verification, Analysis, and Synthesis

with Peleska and Huang

      ü      

Thursday 2 June 2016

216 Bow-Li Hall, National Taiwan Univ., Taiwan, ROC

Co-chairs:

Dr. Churn-Jung Liau

Inst. of Information Science,

Academia Sinica

@

Prof. Farn Wang

Dept. of Electrical Engineering, National Taiwan University

Local Arrangement Chair:

Prof. Farn Wang

National Taiwan University

@

@

Registration

Previous WAVAS':

7th WAVAS on Oct. 20, 2015

6th WAVAS with Professor Huimin LIn on Nov. 28, 2014

5th WAVAS with Holik, Lengal, Lin, and Vojnar on Oct. 25, 2013

4th WAVAS on TaaS on June 28, 2013

3rd WAVAS with Sven Schewe on Oct. 18, 2012.

2nd WAVAS with Gerard Holzmann on April 10, 2012.

1st WAVAS with John Rushby on Feb. 15, 2011@

Aim:

   WAVAS is held to promote collaborations in the research area of automated verification and analysis.  We are happy to announce the fourth WAVAS featuring the techniques and opportunities for our verification researchers in the booming cloud computing.  With the gradual convergence of Interactive Development Environments (IDE) in cloud computing, we can now focus on a few IDEs and expect our innovation be accessible via those IDEs to the app developers.   Thus the opportunity is better than ever for applying formal verification technologies to real-world projects. 

  The 8th WAVAS features invited presentations consist of talks by Professor Jan Peleska and Professor Wen-Ling Huang, luncheon, and coffee breaks. 

Scopes of interest:

Scopes of interests include but are not limited to the following.

Software testing, model checking, proof checking, hardware verification, software verification, timed systems, hybrid systems, complexity, game-theoretical techniques, synthesis, regular system verification.  

Program:

09:00-09:05 Prof. Farn Wang (NTU) Opening
09:10-10:30 Prof. Jan Peleska (University of Bremen and Verified Systems International GmbH)

Industrial verification of avionic, automotive, and railway systems- practical application and theoretical foundations (I)

Abstract:

The verification of safety-critical systems requires considerable effort. For systems of the highest criticality - such as railway interlocking systems, aircraft engine controllers, or anti-lock braking systems in cars - this verification effort is well-known to surpass the development effort, that is, the amount of hours needed to specify, design, and program the software. Since the complexity of safety-critical applications continuously increases, their thorough verification requires automation: otherwise it could never be performed within the tight financial budgets and time frames that are typical for such projects. In this presentation it is highlighted how theoretical foundations in the fields of mathematics and computer science help to solve this problem - sometimes in quite a surprising way: mathematical models originally intended only for increasing the insight into complex system behaviours have been found to be representable in computers and exploitable for automated verification purposes. Starting from practical industrial verification problems, it is highlighted how automated model checking can be applied to verifying highly complex system designs involving concurrency and real-time properties. We show how tests can be automatically generated from mathematical models, so that the whole process of test case identification and test procedure programming can be fully automated, allowing even to prove the correctness of the system under test, under certain hypotheses.

The material presented in this talk is based on projects performed by Verified Systems International, a company providing tools and services for verification and validation of safety-critical systems. The theoretical foundations have been elaborated at the University of Bremen, in collaboration with many research partners world-wide.

@

10:30-11:00 Coffee Break
11:00-12:20
Prof. Jan Peleska (University of Bremen and Verified Systems International GmbH) Industrial verification of avionic, automotive, and railway systems- practical application and theoretical foundations (II)
12:20-14:30 Luncheon
14:30-16:00
Prof. Wen-Ling Huang (University of Hamburg) Testing Safety-Critical Discrete State Systems: Mathematical Foundations and Concrete Algorithms
16:00-16:30 @

Coffee Break

16:30-18:00

Prof. Wen-Ling Huang (University of Hamburg)

Testing Infinite-State Systems: Mathematical Foundations and Concrete Algorithms

Sponsors:

WAVAS thanks the sponsorship of the following affiliations.

Department of Electrical Engineering, National Taiwan University

@

Institute of Information Science, Academia Sinica

@

Contact:

@

Interested colleagues are welcome to submit their papers or slides to Professor Farn Wang of National Taiwan University at farn@cc.ee.ntu.edu.tw

@