AdaCore is pleased to be working with several commercial partners in an effort to create stronger links between academia and the professional Ada community.
Artisan Software
ARTiSAN is committed to creating strong links between academia and industry and has joined AdaCore’s GNAT Academic Program to further this goal. Academic professionals and students will be able to access leading industry toolsets, materials and resources enabling them to share ideas and develop their engineering and programming skills to meet the demanding requirements of industry. We look forward to working with AdaCore and establishing new academic relationships as a result." Jeremy Goulding, CEO.
The ARTiSAN Academic License Program allows accredited universities to equip a classroom, or the whole establishment, with the market leading UML modeling tool: Real-time Studio. Having access to Real-time Studio not only enables students to gain experience in using a powerful object-oriented software engineering tool, but it also allows them to put into practice the UML and object-oriented analysis and design techniques they have learnt equipping them for the challenges they will face upon entering industry.
For further information about ARTiSAN’s Academic Program please send email to education@artisansw.com
IPL
Since the mid-nineties, IPL has offered special licenses to academic institutions to help with undergraduate teaching and postgraduate research (limited to non-commercial projects). They firmly believe that offering their products to academic institutions on favorable terms is of long-term benefit to IPL; it leads to graduates, and ultimately an IT workforce, who understand the value and practice of software testing. Their special academic licence allows students and researchers to benefit from testing tools used by many high profile projects ranging from telecommunications, medical instruments, air-traffic control, avionics, rail transport, automotive, space, defense, nuclear energy, financial to digital broadcast systems. Cantata++ and AdaTEST95 are industry-strength testing tools, used to meet safety critical and high integrity standards such as DO-178B level A, CENELEC, IEC 61508, MISRA. IPL and AdaCore have been working together for many years to ensure that their respective products are properly integrated, and should be appealing to use at both the undergraduate and researcher levels.
For further information about IPL’s Academic Program
please visit:
http://www.ipl.com/products/academic/pa000.uk.php
Praxis High Integrity Systems
The SPARK Language and Tool Set
SPARK is an annotated subset of Ada that is appropriate for the development of high-integrity software systems. The language is designed to have an unambiguous semantics and the annotations add design-by-contract information that enables unprecedented depth and efficiency of analysis and verification to be performed.
The SPARK Toolset implements subset checking, static semantic analysis, information flow analysis, verification condition generation and theorem proving facilities in an industrial strength environment.
For educators, SPARK offers a small language that can be used to teach the principles of design-by-contract, static analysis, formal verification and safety- and security-critical software development. SPARK is also well-suited to the development of real-time and embedded systems. For researchers, SPARK can be used as a basis for advanced verification and analysis technologies, such as software model checking and proof planning. The full professional SPARK toolset is available with support at no cost to university faculty. An excellent textbook, by renowned author John Barnes, is available that explains the SPARK language and technology.
For further information about Praxis’ Academic
Program please visit:
www.praxis-his.com/sparkada/universities.asp
Tidorum
Static analysis of worst-case execution time
The development and verification of real-time software requires knowledge of the execution time of the critical software functions. The execution time is often variable, depending on the input data and program state; what is then required is an upper bound on the worst-case execution time (WCET). Measuring execution times from test cases or profiling runs usually underestimates the WCET. In contrast, a static WCET analysis adds up the WCETs of the instructions on all possible execution paths and uses mathematical optimization methods to compute an upper bound on the total WCET — the longest execution path. Tidorum supplies a tool called Bound-T that uses static analysis of machine code to compute bounds on WCET and stack usage. Bound-T is mainly aimed at the smaller 8- and 16-bit microcontrollers but also supports some 32-bit processors such as the ERC32 (SPARC V7). Tidorum grants no-cost academic licenses for Bound-T and works with academic research groups to develop the tool and WCET analysis in general.
For more information about Tidorum’s academic program please visit:
http://www.bound-t.com/academic.html