TY - GEN
T1 - Formal specification and analysis of active networks and communication protocols
T2 - DARPA Information Survivability Conference and Exposition, DISCEX 2000
AU - Denker, G.
AU - Meseguer, J.
AU - Talcott, C.
N1 - Funding Information:
This work has been partially supported by DARPA through Rome Laboratories Contract F30602-97-C-0312, by DARPA and NASA through Contract NAS2-98073, by ARPA/AirForce under grant F30602-96-1-0300, by NSF under grant CRR-9633419, and by Office of Naval Research Contracts N00014-96-C-0114 and N00012-99-C-0198.
Publisher Copyright:
© 2000 IEEE.
PY - 2000
Y1 - 2000
N2 - Rewriting logic and the Maude language make possible a new methodology in which formal modeling and analysis can be used from the earliest phases of system design to uncover many errors and inconsistencies, and to reach high assurance for critical components. Our methodology is arranged as a sequence of increasingly stronger methods, including formal modeling, executable specification, model-checking analysis, narrowing, and formal proof, some of which can be used selectively according to the specific needs of each application. The paper reports on a number of experiments and case studies applying this formal methodology to active networks, communication protocols, and security protocols.
AB - Rewriting logic and the Maude language make possible a new methodology in which formal modeling and analysis can be used from the earliest phases of system design to uncover many errors and inconsistencies, and to reach high assurance for critical components. Our methodology is arranged as a sequence of increasingly stronger methods, including formal modeling, executable specification, model-checking analysis, narrowing, and formal proof, some of which can be used selectively according to the specific needs of each application. The paper reports on a number of experiments and case studies applying this formal methodology to active networks, communication protocols, and security protocols.
UR - http://www.scopus.com/inward/record.url?scp=84961707449&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84961707449&partnerID=8YFLogxK
U2 - 10.1109/DISCEX.2000.825030
DO - 10.1109/DISCEX.2000.825030
M3 - Conference contribution
AN - SCOPUS:84961707449
T3 - Proceedings - DARPA Information Survivability Conference and Exposition, DISCEX 2000
SP - 251
EP - 265
BT - Proceedings - DARPA Information Survivability Conference and Exposition, DISCEX 2000
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 25 January 2000 through 27 January 2000
ER -