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 proceedingConference contributionAcademic

    27 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 languageUndefined
    Title of host publicationProceedings 49th Conference on Electronic, Telecommunications, Computer science, Automatics, and Nuclear technique, ETRAN 2005
    Place of PublicationBudva, Montenegro
    PublisherCOBISS
    Pages285-288
    Number of pages4
    ISBN (Print)86-80509-53-1
    Publication statusPublished - 2005
    Event49th Conference on Electronic, Telecommunications, Computer science, Automatics, and Nuclear technique, ETRAN 2005 - Budva, Montenegro
    Duration: 5 Jun 200510 Jun 2005

    Publication series

    Name
    Number124996108

    Conference

    Conference49th Conference on Electronic, Telecommunications, Computer science, Automatics, and Nuclear technique, ETRAN 2005
    Period5/06/0510/06/05
    OtherJune 5-10 2005

    Keywords

    • METIS-226473
    • EWI-19766
    • IR-53550

    Cite this