Piter's Home Page

Safety properties state that “something bad never happens” (a program never enters an unacceptable state).

Liveness properties state that “something good will eventually happen” (a program eventually enters a desirable state).

Guarantees specify that an event will eventually happen but does not promise repetitions.

Obligations are disjunctions of safety and guarantee formula

Responses specify that an event will happen infinitely many times.

Persistence specifies the eventual stabilization of a system condition after an arbitrary delay.

Reactivity is the maximal class formed from the disjunction of response and persistence properties.

Unconditional Fairness states that a property p holds infinitely often.

Weak Fairness states that if a property p is continuously true then the property A must be true infinitely often.

Strong Fairness states that if a property A is true infinitely often then the property B must be true infinitely often

Classification of Formal Methods (approaches and tools) according to the types of systems they apply:

* Concurrent systems

o CCS - Calculus of Communicating Systems
o CIRCAL - CIRcuit CALculus
o Concurrency Factory
o CSP - Communicating Sequential Processes
o LOTOS - Language of Temporal Ordering Specifications
o Meije - verification of concurrent programs
o Murphi - description language and verifier tool
o Petri Nets
o Pobl - development method for concurrent object-based programs
o RAISE Method
o TLA - Temporal Logic of Actions
o VeriSoft - model checking tool

* Distributed systems

o Rapide - toolset for large-scale distributed multi-language systems
o SPIN - is an automated verification tool
o UPPAAL
o UNITY - programming notation for parallel and distributed program

* Embedded systems

o HyTech - The HYbrid TECHnology Tool

* Parallel systems

o UNITY - programming notation for parallel and distributed programs

* Reactive systems

o DisCo - specification method for reactive systems
o Esterel - Language and Tools
o LUSTRE - language for programming reactive systems
o TLA - Temporal Logic of Actions
o TTM/RTTL - framework for real-time reactive systems
o VeriSoft - model checking tool

* Real-time systems

o ACSR - Algebra of Communicating Shared Resources
o DC - Duration Calculus
o Kronos - verification tool
o PARAGON - visual specification and verification of real-time systems
o RAISE Method
o TRIO - tools for real-time systems
o TTM/RTTL - framework for real-time reactive systems
o UPPAAL - verification and validation tools for real-time systems
o VeriSoft - model checking tool

* Safety-Critical systems

o NP-Tools - framework for mathematically proving safety properties

* Sequential systems

o ACL2 - A Computational Logic for Applicative Common Lisp
o B-Method
o Boyer-Moore - Theorem Prover
o LARCH
o LOTOS - Language of Temporal Ordering Specifications
o Nqthm - Boyer-Moore theorem prover
o PVS - Prototype Verification System
o RAISE Method
o VDM - Vienna Development Method
o Z notation

* Synchronous systems

o Esterel - Language and Tools
o Signal language

Click to see:

Masha & Petro Image Gallary

SEOUL, South Korea, Aug. 5-10. Computer-science students participating in the Software Design Competition at Imagine Cup 2007 assembled for a week of competition. The 2007 theme, “imagine a world where technology enables a better education for all,” attracted a pool of 100,000 students from 100 countries. Semifinalists include teams representing Austria, China, Czech Republic, Greece, Ireland, Jamaica, Korea, Netherlands, Russia, Serbia, Thailand, and the Ukraine, which will compete in the Worldwide Finals hosted by Joe Wilson, director of Academic Initiatives at Microsoft and Microsoft Corporate Vice President S. Somasegar.

Imagine Cup 2007, Seoul, South Korea - SDI Winners

Team 3KC Returns from Thailand received the First place award in Software Design for their project LiveBook! Members include Prachaya Phaisanwiphatpong, Vasan Chienmaneetaweesin, Jatupon Sukkasem, and Pathompol Saeng-Uraiporn. JPG (104 KB)

Team En#605 received the Second place award in Software Design for their project Finger Code. Members include Lim Chan-kyu, Min Kyoung-hoon, Lim Byoung-su, and Jeong Ji-hyeon.

JPG (78 KB)

Team ICAD from Jamaica received the Third place award in Software Design for their project CADI. Members include Imran Allie, Conroy Smith, Ayson Baxter and Damion Mitchell. JPG (74 KB)
JPG (1.73 MB)

JPG (93 KB)

JPG (2.34 MB)

The Austrian team was selected as an SDI Finalist for their project INTOI Interchange of Ideas.

The team from Ireland (Mark Clerkin, Dan K, Eric McClean and Cathal Coffey) celebrates their selection as an SDI Finalist for their project Signal? Sign Language Learning Environment.

JPG (67 KB) JPG (139 KB)

Students (Ayson Baxter, Conroy Smith, Imran Allie and Damion Mitchell) from the Northern Caribbean University in Jamaica were selected as an SDI Finalist for their project CADI - Computer Aided Distance Instruction. JPG (75 KB)
JPG (166 KB)

Students (Chan-kyu Lim, Byoung-su Lim and Kyoung-hoon Min) from Sejong University in Korea celebrate their selection as an SDI Finalist for their project Finger Code.

JPG (80 KB) JPG (182 KB)

Students (Milan Stojić, Ivan Vujić, Neven Tubić and Sava Čajetinac) from Belgrade University in Serbia were selected as an SDI Finalist for their project DriveON. JPG (67 KB)
JPG (140 KB)

The Thailand team, composed of three students from Kasetsart University and one from Chulalongkorn University, celebrates their selection as an SDI Finalist for their project LiveBooks!

JPG (81 KB) JPG (169 KB)

Students competing in the Software Design Invitational, composed of teams from Austria, Ireland, Jamaica, Korea, Serbia and Thailand, celebrate their selections as Finalists for Imagine Cup 2007. JPG (88 KB)
JPG (200 KB)

Students from University of Applied Science Hagenberg in Austria showcase INTOI? Interchange of Ideas, a hardware-software setup that serves as a hybrid between a digital flipchart and a digital whiteboard. INTOI allows its users to easily write and draw as well as load images, PowerPoint presentations, PDFs and videos.

Zhou Yu, Qi Chen, Jianxin Mao and Sen Li of Team Paladin from China is interviewed about OpenLearning, a set of interactive tools to improve educational resources for students and teachers, especially those lacking resources in remote and rural areas of developing countries.

JPG (74 KB)

The Czech Republic team demonstrates SilentBooks, a program for the hearing impaired that creates 3-D sign language of educational content. JPG (65 KB)
JPG (143 KB)

Students from Aristotle University of Thessaloniki, School of Engineering, Electrical & Computers Engineering Department in Greece, showcase Noesis, a novel educational tool for kids with autism spectrum disorders.

JPG (71 KB) JPG (180 KB)

Mark Clerkin, Dan K, Eric McClean and Cathal Coffey answer questions about Signal? Sign Language Learning Environment, a software solution aimed at educating people in the skill of sign language. JPG (65 KB)
JPG (160 KB)

Students (Ayson Baxter, Conroy Smith, Imran Allie and Damion Mitchell) from the Northern Caribbean University in Jamaica showcase CADI - Computer Aided Distance Instruction, software designed to provide a centralized learning environment for distance education.

JPG (63 KB)

Students (Chan-kyu Lim, Byoung-su Lim and Kyoung-hoon Min) from Sejong University in Korea showcase Finger Code, an educational solution for people with both visual and hearing impairments. JPG (82 KB)

Attendees try out IConnect, a gaming program designed to connect children around the world, breaking down the barriers of language with simple icons. Students from Delft University of Technology in the Netherlands designed the program to help children learn about other cultures.

JPG (73 KB) JPG (185 KB)

Konstantin Kichinskiy, Konstantin Gorskiy, Mikhail Gurenkov and Andrey Sverdlov from Moscow State Aviation Institute in Russia demonstrate Mapedia, a personal knowledge space library. The program uses mind map technology to associate like human thought. JPG (63 KB)

Milan Stojić, Ivan Vujić , Neven Tubić and Sava Čajetinac of Serbia’s Team SMOR demonstrate DriveON. The program, designed by the Belgrade University students, allows student to learn to drive virtually? before getting on the road.

JPG (78 KB) JPG (175 KB)

Comprised of three students from Kasetsart University and one from Chulalongkorn University, team 3KC Returns from Thailand celebrates teamwork for their project LiveBooks! JPG (76 KB)
JPG (183 KB)

Alexey Kuchayev, Valeriy Prokhorov, Petro Protsik and Kirill Yatsenko from Kyiv National University of Tarasa Shevchenka in the Ukraine present Fenestra, a program that allows people with visual disabilities to be fully integrated into the educational process within a normal classroom setting.

JPG (57 KB)

REDMOND, Wash., June 26, 2007? Computer-science students representing Microsoft Imagine Cup 2007 winning teams from 10 world regional finals? Brazil, China, Egypt, France, Germany, Japan, Korea, North America, Poland, United Kingdom? visited Microsoft headquarters in Redmond, Wash., to share their software applications with Microsoft Chairman Bill Gates, Chief Research and Strategy Officer Craig Mundie and Corporate Vice Presidents Sanjay Parthasarathy and S. Somasegar.

Brian Thomas, left, from Tacoma, Wash., explains Team North America’s 2007 Imagine Cup software project Omni to Microsoft Chairman Bill Gates and Microsoft Chief Research and Strategy Officer Craig Mundie. Omni is a language-learning system that uses social networking concepts to encourage student collaboration.

JPG (91 KB) JPG (351 KB)

Microsoft Chairman Bill Gates, center, tries out Team Brazil’s 2007 Imagine Cup software project, KnowTouch, as Microsoft Chief Research and Strategy Officer Craig Mundie looks on. KnowTouch consists of a mobile device with electromechanic pins that accesses a server through radio frequency. Within the servers range, the device receives a list with all the available documents and can turn any of them into Braille. JPG (91 KB)
JPG (407 KB)

Microsoft Chairman Bill Gates (right) and Chief Research and Strategy Officer Craig Mundie receive a demonstration of the Finger Code software project from members of Team Korea. Finger Code is a Braille interpretation system for students who are deaf and blind.

JPG (92 KB) JPG (384 KB)

Microsoft Chairman Bill Gates and Chief Research and Strategy Officer Craig Mundie (second from right) discuss the Openlearning software project with members of Team China. Openlearning is an easy-to-use, unified, adaptable and extensible online learning platform that allows students, teachers and volunteers to connect online and learn from and help one another. JPG (49 KB)
JPG (543 KB)

Microsoft Chief Research and Strategy Officer Craig Mundie (left), Chairman Bill Gates and Corporate Vice President S. Somasegar listen to a presentation of EduCare, a software project from Team Egypt. By providing a fast and efficient communication link between parents, teachers and specialists, EduCare drastically cuts down the time and cost needed to support education for challenged individuals and improves the quality of the education provided to them.

JPG (55 KB) JPG (640 KB)

Microsoft Chairman Bill Gates (left) and Chief Research and Strategy Officer Craig Mundie discuss the re-Educate software project with members of Team France. Through a modern and interactive interface and new technologies such as voice recognition, re-Educate opens up a new world for children with reduced mobility. JPG (47 KB)
JPG (473 KB)

Microsoft Chairman Bill Gates (left), Chief Research and Strategy Officer Craig Mundie and Corporate Vice President S. Somasegar listen to a presentation of UbiZoo, a software project from Team Germany. Through natural history instruction for primary school children and teachers, UbiZoo offers technological support for a visit to the zoo. Through the integration of modern, mobile computers, the visit to the zoo becomes an exciting experience for students and teachers.

JPG (50 KB) JPG (538 KB)

Microsoft Chairman Bill Gates (left) and Chief Research and Strategy Officer Craig Mundie discuss the LinC software project with members of Team Japan. LinC is a system with two solutions: a Learning Management Tool that helps with a student’s learning and a Communication Tool that enables communication with other students. JPG (53 KB)
JPG (547 KB)

Microsoft Chairman Bill Gates (second from left), Chief Research and Strategy Officer Craig Mundie, and Corporate Vice President S. Somasegar listen to a presentation of Onespace, a software project from Team Poland. Onespace enables a group of users to work on a single project at the same time. It provides audio and video communication and enables one to switch between different users’ desktops as easily as switching between applications.

JPG (55 KB) JPG (587 KB)

Microsoft Chief Research and Strategy Officer Craig Mundie (left) and Chairman Bill Gates discuss a presentation of software project First Programme Language from Team UK. First Programme Language (FPL) is designed to develop young children’s problem-solving skills through the teaching of simple programming concepts. JPG (53 KB)
JPG (598 KB)

Link