|
AUTHOR(S): Awwama Emad, Alarsan Mohamed, Kadi Mohammad, Krayem Said, Lazar Ivo, Rihawi Ahmad
|
TITLE |
 PDF |
KEYWORDS verification, rodin, formal modeling, model checking, specification, invariants, context, |
ABSTRACT Philosophy is centrally concerned with arguments. The first question to be asked of any argument (or inference) is whether or not it is valid: that is, does its conclusion really follow from the cited premises? Validity of inference is the central problem of deductive logic. While Rigorous descriptions promise to improve system reliability, design time and comprehensibility, they do so at the cost of an increased learning curve; the mathematical disciplines used to formally describe computational systems are outside the domain of a traditional engineering education. In addition, the meta-models used by most formal methods are often limited in order to enhance provability. There is a notable tradeoff between the need for rigor and the ability to model all behaviors. As formal methods become more common, engineers will have to learn type theory, modern algebra and proof techniques. Ultimately, engineers will have to think more like mathematicians. Event-B is intended to be used to create complex models. Without appropriate tool support this would not be possible. This article presents justifications and explanations for the choices that have been made when designing the Event-B notation. It is used, for discrete systems modelling by refinement |
Cite this paper Awwama Emad, Alarsan Mohamed, Kadi Mohammad, Krayem Said, Lazar Ivo, Rihawi Ahmad. (2017) Using formal methods in signal processing. International Journal of Signal Processing, 2, 41-49 |
