A CSP-based trajectory for designing formally verified embedded control software

D.S. Jovanovic; Geert K. Liet; Johannes F. Broenink

A CSP-based trajectory for designing formally verified embedded control software

D.S. Jovanovic, Geert K. Liet, Johannes F. Broenink

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic

63 Downloads (Pure)

Abstract

This paper presents in a nutshell a procedure for producing formally verified concurrent software. The design paradigm provides means for translating block-diagrammed models of systems from various problem domains in a graphical notation for process-oriented architectures. Briefly presented CASE tool allows code generation both for formal analysis of the models of software and code generation in a target implementation language. For formal analysis a high- quality commercial formal checker is used.

Original language	Undefined
Title of host publication	Proceedings 49th Conference on Electronic, Telecommunications, Computer science, Automatics, and Nuclear technique, ETRAN 2005
Place of Publication	Budva, Montenegro
Publisher	COBISS
Pages	285-288
Number of pages	4
ISBN (Print)	86-80509-53-1
Publication status	Published - 2005
Event	49th Conference on Electronic, Telecommunications, Computer science, Automatics, and Nuclear technique, ETRAN 2005 - Budva, Montenegro Duration: 5 Jun 2005 → 10 Jun 2005

Publication series

Name
Number	124996108

Conference

Conference	49th Conference on Electronic, Telecommunications, Computer science, Automatics, and Nuclear technique, ETRAN 2005
Period	5/06/05 → 10/06/05
Other	June 5-10 2005

Keywords

METIS-226473
EWI-19766
IR-53550

Access to Document

Cite this

@inproceedings{d3d9a1729077441b8c441cabbf1cb445,

title = "A CSP-based trajectory for designing formally verified embedded control software",

abstract = "This paper presents in a nutshell a procedure for producing formally verified concurrent software. The design paradigm provides means for translating block-diagrammed models of systems from various problem domains in a graphical notation for process-oriented architectures. Briefly presented CASE tool allows code generation both for formal analysis of the models of software and code generation in a target implementation language. For formal analysis a high- quality commercial formal checker is used.",

keywords = "METIS-226473, EWI-19766, IR-53550",

author = "D.S. Jovanovic and Liet, {Geert K.} and Broenink, {Johannes F.}",

note = "This research is supported by PROGRESS, the embedded system research program of the Dutch organization for Scientific Research, NWO, The Dutch Ministry of Economic Affairs an the Technology Foundation STW.; 49th Conference on Electronic, Telecommunications, Computer science, Automatics, and Nuclear technique, ETRAN 2005 ; Conference date: 05-06-2005 Through 10-06-2005",

year = "2005",

language = "Undefined",

isbn = "86-80509-53-1",

publisher = "COBISS",

number = "124996108",

pages = "285--288",

booktitle = "Proceedings 49th Conference on Electronic, Telecommunications, Computer science, Automatics, and Nuclear technique, ETRAN 2005",

}

Jovanovic, DS, Liet, GK & Broenink, JF 2005, A CSP-based trajectory for designing formally verified embedded control software. in Proceedings 49th Conference on Electronic, Telecommunications, Computer science, Automatics, and Nuclear technique, ETRAN 2005. COBISS, Budva, Montenegro, pp. 285-288, 49th Conference on Electronic, Telecommunications, Computer science, Automatics, and Nuclear technique, ETRAN 2005, 5/06/05.

A CSP-based trajectory for designing formally verified embedded control software. / Jovanovic, D.S.; Liet, Geert K.; Broenink, Johannes F.
Proceedings 49th Conference on Electronic, Telecommunications, Computer science, Automatics, and Nuclear technique, ETRAN 2005. Budva, Montenegro: COBISS, 2005. p. 285-288.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic

TY - GEN

T1 - A CSP-based trajectory for designing formally verified embedded control software

AU - Jovanovic, D.S.

AU - Liet, Geert K.

AU - Broenink, Johannes F.

N1 - This research is supported by PROGRESS, the embedded system research program of the Dutch organization for Scientific Research, NWO, The Dutch Ministry of Economic Affairs an the Technology Foundation STW.

PY - 2005

Y1 - 2005

N2 - This paper presents in a nutshell a procedure for producing formally verified concurrent software. The design paradigm provides means for translating block-diagrammed models of systems from various problem domains in a graphical notation for process-oriented architectures. Briefly presented CASE tool allows code generation both for formal analysis of the models of software and code generation in a target implementation language. For formal analysis a high- quality commercial formal checker is used.

AB - This paper presents in a nutshell a procedure for producing formally verified concurrent software. The design paradigm provides means for translating block-diagrammed models of systems from various problem domains in a graphical notation for process-oriented architectures. Briefly presented CASE tool allows code generation both for formal analysis of the models of software and code generation in a target implementation language. For formal analysis a high- quality commercial formal checker is used.

KW - METIS-226473

KW - EWI-19766

KW - IR-53550

M3 - Conference contribution

SN - 86-80509-53-1

SP - 285

EP - 288

BT - Proceedings 49th Conference on Electronic, Telecommunications, Computer science, Automatics, and Nuclear technique, ETRAN 2005

PB - COBISS

CY - Budva, Montenegro

T2 - 49th Conference on Electronic, Telecommunications, Computer science, Automatics, and Nuclear technique, ETRAN 2005

Y2 - 5 June 2005 through 10 June 2005

ER -