Profile photo of Vojtěch Forejt
Vojtěch Forejt, Ph.D.
PRECISE Seminar: Automatic Verification of Competitive Stochastic Systems
May 16, 2012

We present automatic verification techniques for the modelling and analysis of probabilistic systems that incorporate competitive behaviour. These systems are modelled as turn-based stochastic multi-player games, in which the players can either collaborate or compete in order to achieve a particular goal. We define a temporal logic called rPATL for expressing quantitative properties of stochastic multi-player games. This logic allows us to reason about the collective ability of a set of players to achieve a goal relating to the probability of an event's occurrence or the expected amount of…

Profile photo of Guo Liang Xing
Guo Liang Xing, D.Sc.
PRECISE Seminar: Wireless Coexistence in Open Radio Spectrum: Curses and Blessings
May 10, 2012

The human world is replete with wireless devices. By their broadcast nature, wireless transceivers often cause significant interference to each other if they use the same frequency. This becomes a growing issue as the open 2.4GHz frequency band is being populated by numerous wireless devices including Wi-Fi access points and handhelds, ZigBee sensors, Bluetooth headsets, and cordless phones. In this talk, I will present our recent work on the coexistence of Wi-Fi and ZigBee. Our study of real-life Wi-Fi networks reveals that abundant /white space/ exists in Wi-Fi traffic. We have developed…

Profile photo of Pavithra Prabhakar
Pavithra Prabhakar, Ph.D.
PRECISE Seminar: Approximations for Verification of Hybrid Systems
April 25, 2012

The increasing demand for automation in safety-critical applications such as aeronautics, automotive, industrial process control, medical devices and so on, has pressurized the need for scalable formal analysis techniques for ensuring reliable and error-free operation of the systems. A unique feature of these systems is the mixed discrete continuous behaviors they exhibit, which is due to the interaction between a digital computer controlling and a physical entity. From the point of view of computability, presence of the continuous dynamics makes the problem challenging so much so that the…

Eric Feron profile photo
Eric Feron, Ph.D.
Joint PRECISE-GRASP Seminar: Proof-Carrying Auto-Coded Control Software
April 13, 2012

Proof-carrying code has been in existence since Necula and Lee coined the term in 1996. This talk brings forward the details of the development of proof-carrying code from control system specifications. The motivation for this work is the safety-critical nature of many control applications such as aeronautics, robot-assisted surgery, and ground transportation. Several challenges must be addressed during this effort, including: The formal representation of control-theoretic proofs; the migration and representation of these proofs across different layers of software implementation; and the…

Profile photo of Paul E. Black
Paul E. Black, Ph.D.
PRECISE Seminar: Combinatorial Testing
February 29, 2012

Studies suggest that nearly all software errors are triggered by the interaction of no more than six parameters.  If so, testing all n-way combinations of parameters should provide high confidence that nearly all faults have been discovered.  This combinatorial testing is already used by dozens of companies.  Dr. Black will explain what combinatorial testing is and how to apply it to different situations.  Given 10 binary variables, can you exercise all triples with fewer than 20 tests?  He refers to free software available to generate such "covering arrays" for combinations of parameter…