Sign In


Sort by AttachmentsUse SHIFT+ENTER to open the menu (new window).
Rigorous Sofware Development via Model CheckingUse SHIFT+ENTER to open the menu (new window).
Gian Luigi Ferrari, Alberto Lluch Lafuente
Software is pervading our lives. Navigation software on our favorite mobile device can prevent us from taking the car due to an unexpected oil loss and plan a convenient route using public transportation. With our software invaded laptop, we can start our work day establishing virtual meetings or performing baking operations. At the end of the lots of software applications have accompanied our social and professional activities. The increase of the role of software as a of full-day companion comes with a price: we depend more and more on it. But, can we trust software? What if a bug in the navigation system drives us to the wrong location? What if misunderstandings arise in our meeting due to a undesirable loss of QoS? What if our banking operations are being hacked? Software reliability is a must, specially when critical issues such as human integrity, privacy or security are involved. Traditionally, the computer science community has promoted the use of formal method as a means to increase the trust that we put on software. Formal specification and verification techniques have been proposed and transfered to industrial-applied technology. While it is honest to admit that not even formally developed software guarantees a complete confidence, it is widely recognized that the use of formal methods increases software reliability. Formal methods are usually seen is an auxiliary tool in software development processes, but our vision promotes the role of formal methods as a companion. Rigorous Software Development must be a formal method. Among the various formal methods we concentrate on Model Checking. Model checking is an automatic formal verification technique whose main idea is to formally specify both the system specification and its properties (typically, by means of temporal logic) and automatically verify that such properties are satisfied. The popularity of model checking has crossed the scientific borders and pervaded the industrial community and, nowadays, model checkers are being used by many companies to produce reliable software. The success of model checking has been sealed with the ACM's Turing award, received by the inventors of such technique. This series of seminars will start with a brief introduction to the fundamentals of rigorous software development and model checking. The rest of the seminars will present various model checkers (such as Spin, SMV) and model checking based development tools (such as Bandera) together with the theoretical models they are based on.
Year: 2008
Period: May - June 2008
PhD Lunchtime SeminarUse SHIFT+ENTER to open the menu (new window).
The Ph.D. Students Lunchtime Seminars are weekly lunch meetings aimed at bringing together the students, researchers and professors in our and other departments to discuss their work. The talks can range from quite informal to formal conference style talks. Just keep in mind the broad computer science audience these talks are thought for.
Year: 2008