View source for Publications:Towards model checking executable UML specifications in mCRL2

<div style='display: none'>
== Do not edit this section ==
</div>
{{PublicationSetupTemplate|Author=Helle Hvid Hansen, Jeroen Ketema, Bas Luttik, Mohammad Reza Mousavi, Jaco van de Pol
|PID=584486
|Name=Hansen, Helle Hvid (Eindhoven University of Technology, Eindhoven, Netherlands);Ketema, Jeroen (University of Twente, Enschede, Netherlands);Luttik, Bas (Eindhoven University of Technology, Eindhoven, Netherlands);Mousavi, Mohammad Reza [mohmou] (Eindhoven University of Technology, Eindhoven, Netherlands);van de Pol, Jaco (University of Twente, Enschede, Netherlands)
|Title=Towards model checking executable UML specifications in mCRL2
|PublicationType=Journal Paper
|ContentType=Refereegranskat
|Language=eng
|Journal=Innovations in Systems and Software Engineering
|JournalISSN=1614-5046
|Status=published
|Volume=6
|Issue=1
|HostPublication=
|Conference=
|StartPage=83
|EndPage=90
|Year=2010
|Edition=
|Pages=
|City=London
|Publisher=Springer London
|Series=
|SeriesISSN=
|ISBN=
|Urls=
|ISRN=
|DOI=http://dx.doi.org/10.1007/s11334-009-0116-1
|ISI=
|PMID=
|ScopusId=2-s2.0-77949321817
|NBN=urn:nbn:se:hh:diva-20519
|LocalId=
|ArchiveNumber=
|Keywords=Executable UML;Model checking;Process algebra;Software verification and validation;Specification languages
|Categories=Data- och informationsvetenskap (102)
|ResearchSubjects=
|Projects=
|Notes=
|Abstract=<p>We describe a translation of a subset of executable UML (xUML) into the process algebraic specification language mCRL2. This subset includes class diagrams with class generalisations, and state machines with signal and change events. The choice of these xUML constructs is dictated by their use in the modelling of railway interlocking systems. The long-term goal is to verify safety properties of interlockings modelled in xUML using the mCRL2 and LTSmin toolsets. Initial verification of an interlocking toy example demonstrates that the safety properties of model instances depend crucially on the run-to-completion assumptions.</p>
|Opponents=
|Supervisors=
|Examiners=
|Patent=
|ThesisLevel=
|Credits=
|Programme=
|Subject=
|Uppsok=
|DefencePlace=
|DefenceLanguage=
|DefenceDate=
|CreatedDate=2013-01-08
|PublicationDate=2013-01-09
|LastUpdated=2013-01-16
|diva=http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:584486}}
<div style='display: none'>

== Keep all hand-made modifications below ==
</div>{{PublicationDisplayTemplate}}