[PPL-devel] [GIT] ppl/ppl(master): Title fixed and abstract added.

[Roberto Bagnara]

Module: ppl/ppl
Branch: master
Commit: 0aa1d092fc001b1aa6accad3a78d8fd7c81377e8
URL:    http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0aa1d092fc001b1aa6accad3a78d8fd7c81377e8

Author: Roberto Bagnara <roberto.bagnara at bugseng.com>
Date:   Sat Dec 28 08:58:20 2013 +0100

Title fixed and abstract added.

---

 doc/ppl_citations.bib |   26 +++++++++++++++++++++++++-
 1 files changed, 25 insertions(+), 1 deletions(-)

diff --git a/doc/ppl_citations.bib b/doc/ppl_citations.bib
index d25ae10..2b3f807 100644
--- a/doc/ppl_citations.bib
+++ b/doc/ppl_citations.bib
@@ -581,11 +581,35 @@ Summarizing:
 
 @Book{AndreS13,
   Author = "{\'E}. Andr{\'e} and R. Soulat",
-  Title = "The Inverse Method: Parametric Verification of Real-time Unbedded Systems",
+  Title = "The Inverse
+           Method: Parametric Verification of Real-time Embedded Systems",
   Publisher = "John Wiley and Sons.",
   Series = "{FOCUS Series}",
   ISBN = "9781118569405",
   Year = 2013,
+  Abstract = "This book introduces state-of-the-art verification
+              techniques for real-time embedded systems, based on the
+              inverse method for parametric timed automata. It reviews
+              popular formalisms for the specification and
+              verification of timed concurrent systems and, in
+              particular, timed automata as well as several extensions
+              such as timed automata equipped with stopwatches, linear
+              hybrid automata and affine hybrid automata.  The inverse
+              method is introduced, and its benefits for guaranteeing
+              robustness in real-time systems are shown. Then, it is
+              shown how an iteration of the inverse method can solve
+              the good parameters problem for parametric timed
+              automata by computing a behavioral cartography of the
+              system. Different extensions are proposed particularly
+              for hybrid systems and applications to scheduling
+              problems using timed automata with stopwatches. Various
+              examples, both from the literature and industry,
+              illustrate the techniques throughout the book.  Various
+              parametric verifications are performed, in particular of
+              abstractions of a memory circuit sold by the chipset
+              manufacturer ST-Microelectronics, as well as of the
+              prospective flight control system of the next generation
+              of spacecraft designed by ASTRIUM Space Transportation."
 }
 
 @Inproceedings{ArmandoBM07,