Book on SysML/MARTE/AADL
This book presents how a common case study (Pacemaker specifications from the pacemaker challenge) can be modeled and analyzed using SysML, UML/MARTE and AADL. It is a joint effort of the french MDE community to compare the different approaches. For each formalism, we propose an introduction to the notation, and then how to model, analyze and generate code from these specifications. Analysis focuses on model checking of the system.
Hence, interested readers can build their own opinion on the value of each approach.