Qualitätssteigerung der Automotive-Software durch formale Spezifikation funktionaler Eigenschaften auf der Abstraktionsebene des Modellentwurfs.