Search w/in this Title for Titles All Reviews
	Formal Methods in System Design Kluwer Academic Publishers         Options: Date Reviewed Title Author Publisher Published Date Descending Order Ascending Order     1-10 of 17 reviews Date Reviewed      Runtime verification of embedded real-time systems Reinbacher T., Függer M., Brauer J. Formal Methods in System Design 44(3): 203-239, 2014.  Type: Article Runtime verification involves checking whether a given system (in software or hardware) satisfies a given property during the execution of the system. This paper presents a set of runtime verification algorithms, their correctness, and... Aug 28 2015   Bounded model checking of infinite state systems Schuele T., Schneider K. Formal Methods in System Design 30(1): 51-81, 2007.  Type: Article Model checking is determining whether a given structure that is derived from hardware or software design satisfies a formal specification. The formal specification is often described as a temporal logic formula. The structure is often ... Jan 18 2008   Model checking with strong fairness Kesten Y., Pnueli A., Raviv L., Shahar E. Formal Methods in System Design 28(1): 57-84, 2006.  Type: Article Classical model checking methods for temporal logic formulas suffer from the problem of unsatisfactory treatment of fairness—only a weak form of fairness, “justice,” is directly addressed. &... Nov 23 2006   Experimental evaluation of verification and validation tools on Martian rover software Brat G., Drusinsky D., Giannakopoulou D., Goldberg A., Havelund K., Lowry M., Pasareanu C., Venet A., Visser W., Washington R. Formal Methods in System Design 25(2-3): 167-198, 2004.  Type: Article Are you responsible for the quality of complex software? Do you look for innovative methods for its verification and validation, or develop advanced tools for this purpose? If so, you should think about reading this paper, about the ef... Sep 2 2005   Static analysis for state-space reductions preserving temporal logics Yorav K., Grumberg O. Formal Methods in System Design 25(1): 67-96, 2004.  Type: Article The problem of automatic verification of programs is a grave one, even for “small” programs, since their semantic models grow not only with the size of the program, but also with the number of variables and ... Aug 3 2005   Predicate abstraction of ANSI-C programs using SAT Clarke E., Kroening D., Sharygina N., Yorav K. Formal Methods in System Design 25(2-3): 105-127, 2004.  Type: Article Predicate abstraction is a method used for checking software systems. One looks for a model with a reduced state space; the original data variables are eliminated, and each predicate is represented by a Boolean variable that represents... Apr 7 2005   Properties of hybrid systems--a computer science perspective Stauner T. Formal Methods in System Design 24(3): 223-259, 2004.  Type: Article In this paper, properties of mixed discrete and continuous systems are clarified for computer scientists, to help them to have a good grasp of corresponding control theory concepts. This authoritatively well-written paper is based on t... Dec 13 2004   Forward analysis of updatable timed automata Bouyer P. Formal Methods in System Design 24(3): 281-320, 2004.  Type: Article Bouyer revisits a well-known forward analysis algorithm for testing state reachability in timed automata, exposing errors in several previously published examinations of the algorithm, and demonstrating its incorrectness in the general... Nov 10 2004   Verisym: verifying circuits by symbolic simulation Adams W., Warren A J., Jamsek D. Formal Methods in System Design 22(2): 163-173, 2003.  Type: Article Adams, Warren, and Jamsek propose a formal verification system, called Verisym, for checking the properties of circuits. The main contribution of the paper is its description of the approach used to check the functional behavior of cir... Jul 21 2004   Mexitl: multimedia in executable interval temporal logic Bowman H., Cameron H., King P., Thompson S. Formal Methods in System Design 22(1): 5-38, 2003.  Type: Article This paper uses an interval temporal logic (ITL) formalism to describe multimedia document constraints, especially those arising from audio and video, based on earlier work by King. This is interesting and innovative.... Jun 11 2004       Display 510152550100 per column
	Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud® Terms of Use | Privacy Policy