Title:Formal validation and requirements management based on the Jackson's reference model

Speaker: Takashi KITAMURA (National Institute of Advanced Industrial Science and Technology (AIST), Japan)

Time: 3:00pm, July 14th(Thursday), 2011

Venue:Lecture Room, Level 3 Building #5, Institute of Software, CAS

Abstract:This research aims to develop a formal framework for (1) formal validation for satisfiability of specifications to requirements, and (2) requirements management based on the Jackson's reference model for requirements and specifications, which provides an insight and perspective basis for relationship between requirements and specifications. To develop the framework, we use propositional logic,
from which we derive formal techniques and devices for computer assistance. In the framework the validation for the satisfiability of specifications with respect to requirements is ascribed to the alidity checking of logical formulas. Also within the framework we develop a notion of ``weakest adequate specifications'' with its calculating technique. We will demonstrate the usefulness of the framework with practical examples.

Biography: Takashi KITAMURA received the B.S. and M.S. degrees in informatics from Shizuoka University, Japan, in 2001 and 2003, respectively.He received the Ph.D. degree of Engineering(computer software and theory) from Institute of Software, Chinese Academy of Sciences in Beijing in 2008.He is currently a post-doctoral researcher in National Institute of Advanced Industrial Science and Technology (AIST) in Japan.