Upcoming Webinars in categories High Security Development

No results found in categories High Security Development

Webinars/Demos in categories High Security Development

  • Introducing SPARK 10.1

    The InSight webinar series continues with a presentation on the new features of the AdaCore/Altran joint offering – SPARK Pro 10.1. SPARK Pro combines the proven SPARK Ada language and supporting toolset with AdaCore’s GNAT Programming Studio (GPS) integrated development environment, backed by unrivalled support systems.

    SPARK 10.1 includes the following enhancements:

    • Generics Phase 1 - Release 10.1 includes the first phase of the addition of support for Ada generics to the SPARK language and toolset
    • Dynamic Flow Analyser and VCG Heaps
    • Unicode characters now allowed in strings
    • Improved use of types and subtypes in FDL
    • Improvements to Simplifier tactics and performance
    • Auto-generation of refinement rules
    • Improvements to SPARKBridge
    • New SPARKClean utility

    This webinar will include a demo and Q&A session with the developers of the SPARK Pro toolset.

  • Introducing SPARK 10

    The InSight webinar series continues with a presentation by Robin Messer on the new features of the AdaCore/Altran joint offering – SPARK Pro 10. SPARK Pro combines the proven SPARK Ada language and supporting toolset with AdaCore’s GNAT Programming Studio (GPS) integrated development environment, backed by unrivalled support systems.

    SPARK Pro 10 is a major release including many new features – automatic selection of flow analysis mode, language profile for SCADE KCG, support for explicitly derived numeric types, addition of the SPARKBridge preview for Windows, library additions, and improvements to the SPARK proof tools.
  • Developing Security-Critical Applications for MLS

    In the aerospace and defense industry there is a growing demand to support high levels of security (Common Criteria EAL4 through EAL7) on critical systems while reducing size, weight, and power (SWaP). To address this demand, there are now commercial-off-the-shelf (COTS) operating system foundations that enable both single level secure (SLS) and multilevel secure (MLS) solutions that speed time-to-market and enable the support of multiple security domains on a single silicon platform.

    However, one of the most challenging components of these solutions is the development of secure applications in these platforms. There is now an open standard, formally defined computer programming language, SPARK, that is designed to support this critical software development process and meet certification requirements of high security software used in applications and systems where predictable and highly reliable operation is essential.

    Join Wind River and AdaCore in this web seminar that unveils the power of COTS solutions and open languages that enable the creation of robust, high security application software for critical systems.
  • Introducing SPARK 9.1

    The InSight webinar series continues with a presentation by Angela Wallenburg on the new features of the AdaCore/Altran joint offering – SPARK Pro. SPARK Pro combines the proven SPARK Ada language and supporting toolset with AdaCore’s GNAT Programming Studio (GPS) integrated development environment, backed by unrivalled support systems.

    SPARK Pro 9.1 is a major release including many new features – the use of full range array subtypes, the relaxation of aliasing rules for record fields, the ability to specify VC generation on a per-file basis in metafiles, the introduction of new SPARK libraries, the introduction of the SPARKbridge feature.
  • Introducing SPARK 9.0

    The InSight webinar series continued with a presentation by Robin Messer on the new features of the AdaCore/Altran joint offering – SPARK Pro. SPARK Pro combines the proven SPARK Ada language and supporting toolset with AdaCore’s GNAT Programming Studio (GPS) integrated development environment, backed by unrivaled support systems.

    SPARK Pro 9 is a major release including many new features – new information-flow verification for safety and security policies, a new SPARK2005 language profile, the new ZombieScope tool, cross referencing annotations in GPS, function return annotations are now treated more like procedure post-conditions, a new output format for POGS, and a new Examiner switch that checks consistency of casing within code and annotations.
  • Getting started with SPARK

    The InSight webinar series continues with a presentation by Rod Chapman on SPARK GPL – the high assurance toolset dedicated to the academic and Free Software communities. SPARK GPL combines the proven SPARK Ada language and supporting toolset with AdaCore’s GNAT Programming Studio (GPS) integrated development environment. SPARK is a language specifically designed to support the development of software used in applications where correct operation is vital either for reasons of safety or security. The SPARK Toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset also generates evidence for correctness that can be used to build a constructive assurance case in line with the requirements of industry regulators and certification schemes.

    This webinar presents the concepts behind the Correctness-by-Construction methodology, includes a demo of the SPARK toolset and will look at current and potential research topics for the academic community.
  • Introducing SPARK Pro

    The InSight webinar series continued with a presentation by Rod Chapman on the AdaCore/Altran new joint offering – SPARK Pro. SPARK Pro combines the proven SPARK Ada language and supporting toolset with AdaCore’s GNAT Programming Studio (GPS) integrated development environment, backed by unrivaled support systems. SPARK is a language specifically designed to support the development of software used in applications where correct operation is vital either for reasons of safety or security. The SPARK Toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset also generates evidence for correctness that can be used to build a constructive assurance case in line with the requirements of industry regulators and certification schemes.

    This webinar presents the concepts behind the Correctness-by-Construction methodology and includes a demo of the SPARK Pro toolset.