Dates and Events: |
OSADL Articles:
2023-11-12 12:00
Open Source License Obligations Checklists even better now
Import the checklists to other tools, create context diffs and merged lists
2022-07-11 12:00
Call for participation in phase #4 of Open Source OPC UA open62541 support project
Letter of Intent fulfills wish list from recent survey
2022-01-13 12:00
Phase #3 of OSADL project on OPC UA PubSub over TSN successfully completed
Another important milestone on the way to interoperable Open Source real-time Ethernet has been reached
2021-02-09 12:00
Open Source OPC UA PubSub over TSN project phase #3 launched
Letter of Intent with call for participation is now available |
COOL - Compact OSADL Online Lectures - November 2024 edition
OSADL talks at ESE Embedded Software Engineering Kongress
COOL - Compact OSADL Online Lectures - December 2024 edition
Real Time Linux Workshops
1999 - 2000 - 2001 - 2002 - 2003 - 2004 - 2005 - 2006 - 2007 - 2008 - 2009 - 2010 - 2011 - 2012 - 2013 - 2014 - 2015
14th Real Time Linux Workshop, October 18 to 20, 2012 at the Department of Computer Science, University of North Carolina at Chapel Hill
Announcement - Call for papers (ASCII) - Hotels - Directions - Agenda - Paper Abstracts - Presentations - Registration - Abstract Submission - Sponsors - Gallery
Alloy: A Language for Modeling and Analyzing Software Systems
Eunsuk Kang, Software Design Group at MIT, USA
Alloy is a modeling language designed for specifying and analyzing software systems. Its underlying toolkit, the Alloy Analyzer, provides fast, automatic analysis that can be used to check a system model against an assertion, detect inconsistencies in a specification, or generate simulation traces. In the past, the tool has been used to model and analyze a variety of systems, including a flash file system, software for smart cards, network and web protocols, a Java virtual machine, Apache server configuration, and social network privacy, among others.
In this talk, I will present an introduction to Alloy, and demonstrate some of its applications. In particular, I will show how the tool can be used to specify and reason about properties of safety critical systems during a development process.
More information about the tool can be found in [1].
