TSE
1998
13 years 10 months ago
1998
—This paper describes three case studies in the lightweight application of formal methods to requirements modeling for spacecraft fault protection systems. The case studies diffe...
CN
2002
13 years 10 months ago
2002
We survey formal methods as they are applied to the development of communication services. We report on industrial and academic projects, consider di erent communication architect...
ASE
2002
13 years 10 months ago
2002
This paper describes a specialized interface to PVS called TAME (Timed Automata Modeling Environment) which provides automated support for proving properties of I/O automata. A maj...
JUCS
2007
13 years 10 months ago
2007
: This introductory paper gives some historical background to the emergence of formal methods, overviews what subsequently happened, and surveys prospects for the future. Brief
FAC
2007
13 years 10 months ago
2007
Abstract. We report on a case study in applying different formal methods to model and verify an architecture for administrating digital signatures. The architecture comprises seve...
JOT
2006
13 years 10 months ago
2006
There are some application domains to which it appears intrinsically challenging to introduce the services offered by formal engineering methods. This paper is an evidence-based p...
ENTCS
2006
13 years 11 months ago
2006
High performance scientific computing software is of critical international importance as it supports scientific explorations and engineering. Software development in this area is...
ENTCS
2006
13 years 11 months ago
2006
The application of formal methods to security protocol analysis has been extensively researched during the last 25 years. Several formalisms and (semi-)automatic tools for the ver...
CORR
2008
Springer
13 years 11 months ago
2008
Springer
Synchronous languages rely on formal methods to ease the development of applications in an efficient and reusable way. Formal methods have been advocated as a means of increasing t...
FMICS
2010
Springer
13 years 11 months ago
2010
Springer
We investigate the application of the software bounded model checking tool CBMC to the domain of wireless sensor networks (WSNs). We automatically generate a software behavior mode...