Title
Specification and formal verification of fuzzy information processing for the case of edge detection
Advisor(s)
Mieczyslaw Kokar
Contributor(s)
Stefano Basagni (1965-), Bahram Shafai, Yaman Yener (1946-)
Date of Award
2009
Date Accepted
8-2009
Degree Grantor
Northeastern University
Degree Level
M.S.
Degree Name
Master of Science
Department or Academic Unit
College of Engineering. Department of Computer and Electrical Engineering.
Keywords
engineering, electronics and electrical, fusion system
Subject Categories
Fuzzy sets, Uncertainty (Information theory)
Disciplines
Electrical and Computer Engineering
Abstract
This thesis explores how an information fusion system can be verified before it is built. Towards this aim, a system is first specified mathematically in a formal language. The specification then can be analyzed by formulating various conjectures (theorems) and proving (or disproving) them using an automatic theorem prover. In our work we use Metaslang as the formal specification language and Specware, which is a tool that supports category theory based algebraic specification of software. One of the most important aspects in information fusion is the uncertainty of the fused decisions that are based on uncertain sources. Out of many possible uncertainty types we focus on fuzzy set theory. We have specified a library of fuzzy set theory that can be used to build specifications of fuzzy information processing systems. As an example, a (fuzzy) edge detection algorithm was implemented and then verified using two theorem provers - Snark and Isabelle. With the help of this approach, reasoning about the impact of the uncertainty of input information is specified formally in every step of the fusion process and can be verified before the system is coded in a programming language.
Document Type
Master's Thesis
Rights Holder
Kemal Keskin
Permanent URL
Recommended Citation
Keskin, Kemal, "Specification and formal verification of fuzzy information processing for the case of edge detection" (2009). Electrical and Computer Engineering Master's Theses. Paper 28. http://hdl.handle.net/2047/d20000030
Click button above to open, or right-click to save.
