Logical Analysis of SBVR Models by First-Order Theorem Proving
Peter Baumgartner (NICTA and ANU)
COMPUTER SCIENCE SEMINAR Logic and ComputationDATE: 2010-11-09
TIME: 15:30:00 - 16:30:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
SBVR (Semantics of Business Vocabularies and Rules) is a standardised controlled natural language for use by business analysts to describe a business from their (non-technical) perspective (1). It is meant to help bridging the gap between informally given regulations and business policies on the one side and implementing compliant IT-based business processes on the other side.
In the talk I will report on initial results on analysing SBVR models for certain properties, like satisfiability, redundancies, and missing definitions. Such analysis is motivated by the need to make sure that SBVR models "make sense" as specification for later implementation. Using first-order theorem proving methods for that is possible because SBVR has been designed with a mathematical-logical semantic in mind.
(1) http://www.omg.org/spec/SBVR/1.0/
BIO:
