Sven Jörges
email: sven.joerges@tu-dortmund.de

Tiziana Margaria

Bernhard Steffen

Under consideration for publication in Formal Aspects of Computing Assuring Property Conformance of Code Generators via Model Checking

Keywords: Extreme Model-Driven Development, Code Generation, Model Checking, Verification

Automatic code generation is an essential cornerstone of today's model-driven approaches to software engineering. Thus a key requirement for the success of this technique is the reliability and correctness of code generators. This article describes how we employ standard model checking-based verification to check that code generator models developed within our code generation framework Genesys conform to (temporal) properties. Genesys is a graphical framework for the high-level construction of code generators on the basis of an extensible library of well-defined building blocks along the lines of the Extreme Model-Driven Development (XMDD) paradigm. We will illustrate our verification approach by examining complex constraints for code generators, which even span entire model hierarchies. We also show how this leads to a knowledge base of rules for code generators, which we constantly extend by e.g. combining constraints to bigger constraints, or by deriving common patterns from structurally similar constraints. In our experience, the development of code generators with Genesys boils down to re-instantiating patterns or slightly modifying the graphical process model, activities which are strongly supported by verification facilities presented in this article.

Introduction

Automatic code generation is a key feature of model-driven approaches to software engineering. It has several advantages such as the elimination of manual coding errors, and it provides a fast track to a deployable and testable system/application. Furthermore, it disburdens developers from writing boilerplate code, which is often a highly repetitive and cumbersome task, and by doing this, it shifts the attention back to the primary concern, the application-level logic. Of course, an indispensable requirement for the success of this approach is the reliability and correctness of the corresponding code generators.

In [START_REF] Jörges | Genesys: Service-Oriented Construction of Property Conform Code Generators[END_REF], we presented Genesys, a framework for the high-level construction of code generators along the lines of the Extreme Model-Driven Development (XMDD, see Sect. 2) paradigm. In this framework, code generators are modeled on the basis of an extensible library of well-defined building blocks. We showed that constructing code generators this way offers several advantages, such as the high potential for reuse: The building blocks, as well as whole parts of code generators covering features or aspects like error-handling or input/output-related tasks, can easily be reused for constructing new code generators. This enables short development cycles and a fast evolution of the generation library. We also showed that the approach perfectly integrates with other classical, well-established concepts, such as bootstrapping from the field of compiler construction.

In this article we focus on another advantage. The XMDD approach comprises model checking-based [CGP01, QS82] verification, which can be applied to the code generators: As the code generators are realized as formal models, they are amenable to such techniques. This enables us to check code generation rules or constraints, e.g. guaranteeing the complete processing of all input data or the correct order of generation steps. Genesys contains a large and steadily growing library of such constraints, which greatly improves the overall quality and reliability of the code generators.

In [START_REF] Jörges | Genesys: Service-Oriented Construction of Property Conform Code Generators[END_REF], we already briefly motivated the use of model checking in Genesys with several simple example constraints. As the main contribution of this article, we want to elaborate on this by examining more complex constraints for code generators, which even span entire model hierarchies. We also show how we constantly extend our knowledge base for code generation by e.g. combining constraints to bigger constraints, or by deriving common patterns from structurally similar constraints. For our experiments, we used the model checker GEAR [START_REF] Bakera | Property-driven functional healing: Playing against undesired behavior[END_REF][START_REF] Bakera | Verification, diagnosis and adaptation: Tool supported enhancement of the model-driven verification process[END_REF] to check whether the code generators conform to the constraints, which we specified graphically using the FormulaBuilder [START_REF] Jörges | FormulaBuilder: A Tool for Graph-based Modelling and Generation of Formulae[END_REF][START_REF] Jörges | Genesys: Service-Oriented Construction of Property Conform Code Generators[END_REF].

In our experience, the development of code generators with Genesys boils down to re-instantiating patterns or slightly modifying the graphical process model. These activities are strongly supported by the application of model checking presented in this article, as it helps leveraging the increasing body of domain knowledge during code generator construction.

In the following sections, we first will describe jABC, which is a basic framework that enables the development according to XMDD (Sect. 2). Afterwards, we present Genesys, which is based on the jABC (Sect. 3), and we briefly recapitulate the main ideas presented in [START_REF] Jörges | Genesys: Service-Oriented Construction of Property Conform Code Generators[END_REF]. Sect. 4 outlines the verification facilities of the jABC, which we apply to check the property conformance of Genesys' code generators. Subsequently Sect. 5, the main section, describes and exemplifies the verification of code generators along an elaborate example. Finally, we discuss some related work (Sect. 6), before we conclude with Sect. 7.

The jABC Framework

The code generation framework Genesys is an integral part of jABC, which follows the ideas of Extreme Model-Driven Development (XMDD) [START_REF] Margaria | Agile IT: Thinking in User-Centric Models[END_REF]. XMDD is a new development paradigm designed to continuously involve the customer/application expert throughout the whole system's life cycle. In technical practice, userlevel models are successively enriched and refined from the user perspective, until a sufficient level of detail is reached. At this level, elementary services, solving tasks at the application level, can be implemented. The realization of the individual services should typically be simple and is often based on functionality provided by third-party and standard software systems. As the continuously enriched model is the central and sole artifact of this methodology, which comprises all relevant information including documentation, access policies, versioning, etc., we also call this the "One-Thing Approach" [START_REF] Steffen | Full Life-Cycle Support for End-to-End Processes[END_REF][START_REF] Margaria | Business Process Modelling in the jABC: The One-Thing Approach[END_REF].

jABC is a flexible framework designed to support systematic development according to the XMDD paradigm (see Fig. 1). It allows users to develop service-oriented systems by composing reusable building blocks into flow graph structures, called Service Logic Graphs (SLG). The building blocks are called Service Independent Building Blocks (SIBs) [START_REF]General recommendations on telephone switching and signaling -intelligent network: Introduction to intelligent network capability set 1[END_REF][START_REF]Intelligent Network -Global Functional Plane Architecture[END_REF], and may represent a single atomic service or also a whole subgraph (i.e. another SLG, called features in Fig. 1). Thus SLGs can be hierarchical, which facilitates the refinement along the lines of the One-Thing Approach. This also grants a high reusability not only of the building blocks, but also of the models themselves, within larger systems. Besides SIBs and hierarchical SLGs, there are constraints defining e.g. the structure of the underlying meta model, global frame conditions and business rules, and which can be verified by formal methods like model checking (see Sect. 4). Finally, the modeled SLG can be compiled to a stand-alone running system. This compilation part is the task of Genesys. Furthermore, an extensible set of jABC plugins provides additional functionality that adequately supports all the activities needed along the development lifecycle.

Fig. 2 shows a screenshot of jABC's user interface. The GUI consists of three main parts (indicated by the numbers):

1. the project & SIB explorers, which enable the user to browse available jABC projects and the library of building blocks that can be used for modeling, 2. the graph canvas, which is used for composing SLGs, and 3. the inspectors, which provide detailed information about selected SIBs and may be used by plugins to add further functionality.

Several application domains have been successfully covered with the jABC, including complex supply chain management with IKEA [HMM + 08], modeling and execution of bioinformatics workflows [START_REF] Margaria | Bio-jeti: a service integration, design, and provisioning platform for orchestrated bioinformatics processes[END_REF], the Semantic Web Service challenge [START_REF] Kubczak | Service-oriented Mediation with jABC/jETI[END_REF], dataflow analysis of Java programs [START_REF] Lamprecht | Data-flow analysis as model checking within the jabc[END_REF], a management framework for remote intelligent configuration of systems [START_REF] Bajohr | Matrics: A service-based management tool for remote intelligent configuration of systems[END_REF], online decision support systems [START_REF] Karusseit | Feature-based modelling of a complex, online-reconfigurable decision support service[END_REF] and graphical construction of game strategies [START_REF] Bakera | Test your Strategy: Graphical Construction of Strategies for Connect-Four[END_REF]. These projects were very different in nature, nevertheless we observed a surprisingly high potential of synergy, which was due to the XMDD approach.

In the following sections, we will elaborate on how SIBs and SLGs are defined, constructed and organized.

Service Independent Building Blocks (SIBs)

A SIB is an abstract and generic representation of some service or functionality. In order to provide configurability, each SIB contains a set of formal parameters. Via those parameters, a SIB's behavior can be customized depending on the current context of use. In a model, SIBs are then wired based on the possible results of their execution, reflected by a list of outgoing branches. Roughly speaking, branches can be considered the "exits" of a building block. SIBs and their constituents are described using simple Java classes.

For the graphical representation to the jABC user, each SIB consists of an icon and a documentation of its constituents and its purpose. Furthermore, SIBs are semantically classified in terms of taxonomies. A taxonomy is a directed acyclic graph: sinks represent SIBs, which are atomic entities in the taxonomy, and intermediate nodes represent groups, that is sets of modules satisfying some basic property (expressed as predicates). This structure is freely defined by domain experts, who organize, label and preconfigure SIBs so that they fit the actual domain.

A SIB's implementation (i.e. its execution behavior) is realized by one or more service adapters. Each service adapter contains execution code for a particular SIB. In most cases, this includes data type conversions and calls to third-party libraries that implement the runtime functionality of the SIB. As a SIB's execution behavior may be different depending on the execution environment, an arbitrary number of service adapters can be assigned to one SIB. For instance, imagine a SIB that reads in customer data for a shop application: in a staging or testing environment, this information might come from a text file containing dummy data, whereas in a live scenario the customer data might be stored in a database system. These different behavioral patterns would be realized by two service adapters, one for the staging system and one for the live system. Service adapters assure that the execution of a SIB is entirely platform-independent: the same SIB may be executable in a standard Java environment, a .NET setup and on a mobile phone, if it provides corresponding service adapters. Thus from the modeling perspective, the usage of a SIB completely virtualizes the target platform on which it will be executed.

Fig. 2 contains an example of a SIB and its constituents. In the canvas (2), we highlighted a SIB instance labelled "Write Method Header". This is an instance of the SIB "RunVelocity", which can be found inside the taxonomy displayed in the SIB explorer (1). In this taxonomy, the SIB is labeled as part of the "Script SIBs", which in turn are classified as "jABC Common SIBs". The latter denotes a big SIB library that is shipped with jABC, and that provides ready-made SIBs for very general, typically quite low-level functionality useful for almost any application [START_REF]jABC Common Sibs[END_REF]. The task of the "RunVelocity" SIB is to employ the Velocity template engine [START_REF]Velocity Website[END_REF] to evaluate a template, which is specified by setting one of the SIB's parameters. Such a template is written in the Velocity Template Language (VTL), and is basically a textual skeleton containing placeholders which are filled with dynamic content as soon as the SIB is executed. Afterwards, the result of the evaluation is pushed into the so-called execution context. For the scope of this article, it is sufficient to think of the execution context as a shared memory, which allows SIBs to communicate with each other during the execution.

As visible from the SIB inspector in Fig. 2 (3), the "RunVelocity"-SIB takes three parameters:

• template: The Velocity template to be evaluated. In the case of the "Write Method Header" instance, this template is used to generate the signature and first lines of a Java main method. • result: The key which is used to store the evaluation result in the execution context. For "Write Method Header", this key is bufferMethod. • append : If this boolean flag is set to true, and if there is already a buffer in the execution context identified by the key "result", the evaluation result is appended.

Furthermore, the SIB has two branches (not visible in Fig. 2): default, if the template was evaluated successfully, and error, if the template could not be evaluated (e.g. because of syntax errors). As most of Genesys' code generators are template-based, the "RunVelocity" SIB is used very frequently in this context.

Service Logic Graphs (SLGs)

In the jABC, Service Logic Graphs (SLGs) are internally modeled as Kripke Transition Systems (KTS, [START_REF] Müller-Olm | Model-Checking: A Tutorial Introduction[END_REF]) whose nodes represent elementary SIBs and whose edges represent branching conditions (see Fig.

2):

Definition 1 (Kripke Transition System, KTS). A KTS (V, AP, I, Act, →) consists of a set of nodes V and a set of atomic propositions AP describing basic properties for a node. The interpretation function I : V → 2 AP specifies which propositions hold at which node. A set of action labels Act is used to designate branching conditions. The possible transitions between nodes are given by the relation

→ ⊆ V × Act × V .
Through this non-standard abstraction in our model we obtain a separation of concerns between

• the control-oriented modeling layer, where the user is not troubled with implementation details while designing or evaluating the applications, and • the underlying data-oriented communication mechanisms enforced between the participating subsystems, which are hidden in the SIB implementation.

As a key characteristic, jABC facilitates hierarchical design. SLGs are allowed to make full use of other already existing SLGs (cf. [START_REF] Steffen | Hierarchical service definition[END_REF] for a detailed discussion). Fig. 3 shows an example of a hierarchical SLG with a three-level hierarchy: SIBs with a green dot in the middle (e.g. "GenerateSIBGraphCells") are so-called macros which reference a submodel and thus realize hierarchy. Just like any other SIB, such a macro has parameters (model parameters) and outgoing branches (model branches). The parameters of a macro can be mapped to (selected) parameters of the underlying SIBs. Similarly, the set of (un-set) outgoing branches of the underlying SIBs defines the outgoing branches of the macro. For a detailed description of the hierarchical SLG in Fig. 3 please refer to Sect. 3. Please note that, in contrast to comparable approaches like e.g. the Business Process Execution Language (BPEL, [START_REF]WS-BPEL 2.0 Specification[END_REF]), a big advantage of SLGs is their direct and clean formal semantics.

The Genesys Framework

Once the SLG of a system or application is fully designed and all SIBs are implemented, it is ready for deployment. The SLG has to be transformed into an executable and deployable artifact, usually a piece of code in a desired programming language suitable for a particular execution environment. This is the task of Genesys [START_REF] Jörges | Genesys: Service-Oriented Construction of Property Conform Code Generators[END_REF], which provides means for the construction of highly specialized code generators that are made available to the user via a jABC plugin.

Furthermore, Genesys is a framework that enables the construction of code generators along the lines of XMDD. Accordingly, all code generators in Genesys are themselves designed and built as SLGs within the jABC. In [START_REF] Jörges | Genesys: Service-Oriented Construction of Property Conform Code Generators[END_REF], we already described this concept, and we also discussed the various advantages arising from it, such as the possibility of bootstrapping and a high potential for reuse of already existing components. As the focus of this article is rather on the verification of Genesys' code generators, we will only provide a short overview of the main ideas and concepts presented in [START_REF] Jörges | Genesys: Service-Oriented Construction of Property Conform Code Generators[END_REF].

Bootstrapping & Evolution Via a jABC plugin called Tracer [SMN + 06], SLGs can be directly executed (animated), which enables rapid prototyping and debugging of modeled systems. In other words: the Tracer is an interpreter for SLGs, which also enables the immediate execution of code generators modeled in jABC. This allows us to perform bootstrapping: by tracing a code generator's SLG, we can apply this code generator to itself and gain the same code generator, implemented in another language. The further evolution then mostly boils down to simple parameterization: As currently most of the generators provided by Genesys are template-based, the typical way to build a new generator is to modify the templates (that is, to parametrize the SIBs) of an existing generator accordingly.

Reuse of Components

In [START_REF] Jörges | Genesys: Service-Oriented Construction of Property Conform Code Generators[END_REF], we described the genealogy of Genesys' code generators, showing how the different generators emerged from each other. Corresponding to the ideas of XMDD, a rich pool of existing components accelerates the development of new code generators. These components can be:

• SIBs, which mostly come from jABC's Common SIBs (see 2.1), or in rare cases have to be newly implemented, and • SLGs, which model features or aspects that are reusable among different code generators.

For instance, we derived a code generator for C# by almost entirely reusing a code generator for Java Servlets. Besides parameterization of contained SIBs and SLGs (e.g. modification of templates to contain C# rather than Java syntax), virtually no modifications of the SLG's workflow were necessary.

Extruders & Pure Generators During the early development of Genesys, we recognized that the code generators can be divided into two different classes: Extruders and Pure Generators. These classes differ in the applied strategies for mapping SLGs into executable source code, as well as in the extent to which jABC features are required for the execution of the generated source code.

Generators belonging to the Extruder class simply use the Tracer for the execution of the generated code. This is perfectly possible as the Tracer provides an API for interpreting SLGs without the jABC user interface. Furthermore, Extruders directly use jABC's graph data structures to represent the SLGs in the generated code. Both, the use of the Tracer as well as the use of jABC's data structures, cause the generated code to depend on the jABC framework during compilation and runtime. Furthermore, the execution with the Tracer causes some runtime overhead. All this may be problematic for application domains with strong performance requirements or memory limitations as it is often the case for embedded systems.

The big advantage of Extruders is their simplicity, as they support all advanced Tracer features, like e.g. thread and event handling. Furthermore, Extruders automatically profit from every new Tracer feature. For Pure Generators, neither the jABC Tracer nor the jABC Framework are required. They solely base on functionality provided by the considered runtime environment, like e.g. the Java Runtime Environment (JRE). Moreover, code produced by Pure Generators is usually smaller and faster. These advantages come of course at a rather high price: to profit from complex Tracer features, they need to be specifically programmed. Fig. 3 shows a hierarchical SLG that models a part of a code generator for Java classes. This SLG is shared by all code generators following the Extruder approach and targeting a Java-based platform (such as the Java Standard Edition, JSE). The depicted SLG hierarchy is responsible for processing the input SLGs for which code will be generated. In the Extruder approach, a Java method is generated for each input model. Each method then contains code for all constituents of an SLG, e.g. for SIBs, parameters, edges, etc. When such a method is executed, it basically reconstructs the corresponding SLG using jABC's graph data structures, which is understood by and passed to the Tracer. Please note that the depicted SLG hierarchy is truncated for the sake of presentability. This is sufficient as our example focuses on the generation of code for SIB parameters, leaving out all the other constituents of an SLG.

The SLG marked with number 1 in Fig. 3 first iterates over all input models (SIB "Next Model"). Via an instance of the "RunVelocity" SIB introduced in Sect. 2.1, it then generates the header of the method ("GenerateMethodHeader"). Afterwards, there are two macros (see Sect. 2.2) containing further SLGs that generate code for the SIBs (the SLG marked with 2), for the SLG's edges and for its model parameters. Finally, another "RunVelocity" SIB is used to generate the remainder of the method ("GenerateMethod-Footer").

SLG 2 is responsible for generating code for all SIBs contained in an input model. First, the current input model and its SIBs are retrieved. Afterwards, the SLG simply iterates over the SIBs ("Next SIB Graph Cell"), and generates code for each by calling SLG 3, which is again embedded via a macro. SLG 3 first retrieves the current model, the current SIB and its parameters. Then it iterates over the SIB's parameters ("Next SIB Parameter") and generates corresponding code via "RunVelocity" SIBs, depending on whether the current parameter is a normal SIB parameter ("GenerateSIBParameter") or exported as a model parameter ("Generate SIB Model Parameter").

For this article, it is not necessary to understand all details of this code generation process. The modus operandi of all Genesys code generators is pretty standard: The generator reads the input models and then iterates all contained elements in order to retrieve all information necessary to produce corresponding code. However, the example in Fig. 3 provides an impression of how such generation processes are expressed as jABC models, and finally forms the basis for the case study presented in the following sections.

Besides the advantages given above, the Genesys approach to the development of code generators also enables the use of sophisticated verification techniques like model checking, which we already motivated in [START_REF] Jörges | Genesys: Service-Oriented Construction of Property Conform Code Generators[END_REF]. In Sect. 5, we will further elaborate on how we used model checking to assure the property conformance of code generators.

Model Verification

As visible from Fig. 1, safeguarding the consistency and compatibility during the integration of a system is key to the XMDD paradigm. Thus constraints or business rules, which usually arise from the given application domain, have to be defined. While assembling a global system SLG from SIBs, macros and other SLGs, these constraints have to checked continuously, in order to ensure that the created system is executable and translatable to working code.

For the verification of SLGs, we distinguish between local and global constraints. jABC allows to check In the following, we will briefly introduce both types of constraints and the respective check tools.

Checking Local Constraints with the LocalChecker

Local constraints relate to specific parts of the application, i.e. to its components. In the context of SLGs, these components are the SIBs used for modeling. Constraints for SIBs usually have to do with e.g. correct parameterization, the valid assignment of branches etc. Such simple local conditions are verified using the LocalChecker [SMN + 06] plugin of jABC. The check conditions are explicitly implemented in the Java class representing a SIB. If conditions are not fulfilled while modeling, the LocalChecker immediately informs the user with messages categorized according to their severity, e.g. as warnings, errors or fatal errors, as displayed on the left side of Fig. 4. This ensures the correct usage of building blocks and thus prevents common modeling mistakes.

For assuring the correct appliance of SIBs in Genesys' code generators, we enforce the use of all standard checks that are provided out-of-the-box by the LocalChecker. This impedes common modeling errors such as edges without any targets (which is tantamount to a breach in the execution flow), missing branch assignments (leading to inaccessible execution paths) or the use of SIBs which are not suitable for building code generators (because they e.g. originate from another, incompatible application domain).

An important example of using local checks is the "RunVelocity" SIB. As already outlined in Sect. 2.1, this SIB takes a Velocity template as a parameter. One necessary local check of course is to check for the bare existence of a corresponding template, another application is to check the validity of the template's syntax. A result from the latter check is visible in Fig. 4: The first message in the inspector on the left reports a syntax error in the Velocity template belonging to the SIB "Generate Main Method Header", which can be found in the SLG on the right. Fig. 4 also exemplifies several other messages typically emitted by the LocalChecker. As a further example, we use local checks to control whether certain project guidelines are followed properly. For instance, SIBs which are not documented always lead to a warning.

Checking Global Constraints with GEAR

In contrast to local constraints, global constraints usually span the entire application, sometimes even the whole domain or frame conditions enforced by the corresponding meta model. The ideas formulated by such constraints seem often very simple, as they mostly require the consistency between actions taken at different points of the configuration or functioning of the system, e.g. in order to guarantee well-formedness, executability etc.

Take for instance the "RunVelocity" SIB we presented in Sect. 2.1, which demands a Velocity template as a parameter. Of course, it is essential for a code generator which e.g. generates Java code, that only SIBs that specify Java Templates are used -a constraint which has to be satisfied in order for the code generator to work properly.

If the system is designed in a model-driven way, there are automated ways of proving this consistency of actions. Model checking [CGP01, QS82] is a powerful approach to automatic verification of behavioral models, as it provides an effective way to determine whether a given system model is consistent with a specified (temporal) property. The jABC framework incorporates this technique via the model checker GEAR [START_REF] Bakera | Property-driven functional healing: Playing against undesired behavior[END_REF][START_REF] Bakera | Verification, diagnosis and adaptation: Tool supported enhancement of the model-driven verification process[END_REF], which is integrated as a plugin. Intuitively, any system modeled as SLGs can be verified with this tool: As described in Sect. 2.2, SLGs can be seen as KTS including atomic propositions and actions. Please note that the results presented below are not restricted to the use of GEAR -any model checker such as SPIN [START_REF] Holzmann | The SPIN Model Checker : Primer and Reference Manual[END_REF] or SMV [START_REF] Clarke | Model Checking[END_REF] could be easily integrated into jABC using its plugin mechanism.

Global constraints usually are defined using appropriate formalisms. In the case of GEAR, these are temporal logics, for example CTL (Computation Tree Logic). As we will use CTL for textually describing the constraints that are to be discussed later on in Sect. 5, we will now briefly introduce the logic.

CTL can be used to formulate temporal constraints of a model which e.g. are concerned with the reachability of certain states. For the specification of such formulas CTL offers the path quantifiers A and E as well as the temporal operators F, U (and its weak variant WU ), X and G. CTL belongs to the branching-time logics, i.e. its temporal operators quantify over computation paths that start in a specific state of the model. CTL formulas can be constructed as follows (p represents atomic propositions):

φ ::= p | ¬φ | φ 1 ∨ φ 2 | EXφ | EGφ | E[φ 1 U φ 2 ]
The intuition behind these operators is as follows: the validity of an atomic proposition p is checked relative to a valuation function associating atomic propositions with states. The following two operators are the standard negation and disjunction, while

• EXφ requires φ to hold in one successor state, • EGφ requires φ to hold continuously along one leaving path, and • E[φ 1 U φ 2 ] requires φ 1 to hold until φ 2 eventually holds along one leaving path.

For the formal semantics of CTL formulas please refer to [START_REF] Clarke | Model Checking[END_REF].

With the help of the minimal grammar given above, all the other CTL operators can easily be constructed [START_REF] Clarke | Model Checking[END_REF]:

φ 1 ∧ φ 2 ≡ ¬(¬φ 1 ∨ ¬φ 2 ) φ 1 ⇒ φ 2 ≡ ¬φ 1 ∨ φ 2 AXφ ≡ ¬EX(¬φ) EF φ ≡ E[true U φ] AGφ ≡ ¬EF (¬φ) AF φ ≡ ¬EG(¬φ) A[φ 1 U φ 2 ] ≡ ¬E[¬φ 2 U (¬φ 1 ∧ ¬φ 2 )] ∧ ¬EG(¬φ 2 ) A[φ 1 W U φ 2 ] ≡ ¬E[¬φ 1 U ¬φ 2 ] E[φ 1 W U φ 2 ] ≡ ¬A[¬φ 1 U ¬φ 2 ]
The A[φ 1 W U φ 2 ] will be used in the complex constraints discussed in Sect. 5. It denotes a weak variant of the until operator, that requires φ 1 to hold until φ 2 holds along all leaving paths. Please note that in contrast to the strong until operator, φ 2 is not required to occur in cases where φ 1 continues to hold indefinitely.

GEAR also supports the specification of constraints using other logics like e.g. Allen's Temporal Logic (ATL, [START_REF] Allen | Maintaining knowledge about temporal intervals[END_REF]). Internally, these input logics are mapped to modal µ-calculus [START_REF] Kozen | Results on the Propositional mu-Calculus[END_REF]. Furthermore, GEAR's input syntax is extensible via so-called macros (not to be confused with macro SIBs that are used for hierarchical SLGs!). Basically, a macro is an abbreviation or a pattern that represents a specific formula, thus leading to more readable and concise formulas. For instance, GEAR's macro mechanism is used to incorporate the property specification patterns proposed by Dwyer et. al. [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification[END_REF], and it is also used for mapping CTL and ATL to modal µ-calculus.

To further ease the specification of constraints, a tool called the FormulaBuilder [JMS06, JMS08] enables users to model the constraints themselves as SLGs. Users can thus create both the system and the constraints in the same environment. As such graphically modeled constraints are a special kind of SLG, we call them formula graphs. In comparison to normal SLGs there are two restrictions on formula graphs. First, as formula graphs reflect the syntactic structure of constraints, they usually are trees or directed acyclic graphs. Second, only specific SIBs, called Formula Building Blocks (FBBs) can be used to model constraints this way. FBBs represent the parts of a formula, i.e. operators, operands, etc. The FormulaBuilder provides a large library of FBBs for creating constraints, including logical, arithmetic, comparison and set operators as well as all specification patterns and other GEAR macros. Furthermore, jABC's hierarchy feature allows the creation of composite constraints and new patterns. We will elaborate on this later on in Sect. 5.

Fig. 5 shows an example of how we use GEAR and the FormulaBuilder for checking the Java Class Extruder, whose topmost SLG is depicted on the bottom right of the image. The graph on the top right represents a constraint that will be translated by the FormulaBuilder into the following formula meaning "From an iterator that processes SLGs, an iterator that processes SIBs has to be reachable via the 'next' branch.":

IterateSLGs ⇒ < next > EF (IterateSIBs)
In this formula, < conditions > φ indicates the diamond operator (originating from Hennessy-Milner logic [START_REF] Hennessy | Algebraic laws for nondeterminism and concurrency[END_REF][START_REF] Milner | Communication and Concurrency[END_REF]), while conditions represents an (optional) set of branch names. The given formula is true, if φ holds for at least one of the successor states reachable via a branch specified in conditions.

This formula graph can be dragged into the GEAR inspector depicted on the bottom left of Fig. 5. It is then added to the constraint library of the Java Class Extruder and translated on-the-fly by the FormulaBuilder, each time the constraint is required. Via the GEAR inspector and while modeling, the user is always able to check whether all constraints attached to an SLG and its sub-models are currently satisfied. In the following section, we will discuss more complex constraints used to verify Genesys' code generators.

Checking the Property Conformance of Code Generators

As the main contribution of this article, this section will focus on how we use jABC's verification facilities (outlined in Sect. 4) to support quality and reliability in the Genesys framework.

Sect. 4.1 already exemplified the application of the LocalChecker in the context of Genesys. In the following, we will concentrate on the verification of code generators via the model checker GEAR. In [START_REF] Jörges | Genesys: Service-Oriented Construction of Property Conform Code Generators[END_REF] we already provided some simple example constraints that motivated the usage of model checking-based verification in the context of Genesys. We will further elaborate on this by examining more complex constraints, which span entire model hierarchies.

These constraints are part of a library of requirements which apply to all SLGs contained in Genesys. Since the publication of [START_REF] Jörges | Genesys: Service-Oriented Construction of Property Conform Code Generators[END_REF], this library of constraints has been steadily growing. This is due to the fact that new code generators usually raise new constraints, which then are added to the library and often can even be reused and recombined for checking other code generators. The following sections will also show how we modularized constraints in order to broaden their applicability.

As motivated in [JMS08], jABC's integrated model checker GEAR (see Sect. 4.2) enables checking global constraints that address the well-formedness of the SLGs contained in Genesys. These constraints are collected in a library, which serves as a corpus of rules and guidelines for constructing code generators. There are several occasions which cause this library to grow steadily, e.g.:

• A new code generator is developed and raises new constraints.

• A bug that traces back to a modeling mistake which has been found in a code generator. A new constraint is then added to the library to assure that such mistakes will not happen again. • Existing constraints are recombined to form new, in most cases stronger and more strict, constraints.

As depicted in Fig. 5 at the top left, the library is organized according to the constraint's semantics. This structure is inspired by the structure of the well-known specification pattern system presented by Dwyer et. al in [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification[END_REF]. Accordingly, most constraints are currently distinguished by whether they say something about the occurrence of actions ("actionOccurrence") or the relative order ("actionOrder").

Occurrence Constraints

Fig. 6 shows three example constraints belonging to the category actionOccurrence. The depicted formula graphs represent the following constraints (translated into natural language and into a syntax close to GEAR's input syntax; the numbering corresponds to Fig. 6):

(1) All errors are handled or at least logged, otherwise the generation fails or finishes successfully: In constraint (1), the subformula using the diamond operator demands that every node in the SLG has an outgoing edge labeled with the branch error and pointing to a valid successor, while GenerationSuccessful, GenerationFailed and Log are atomic propositions. An early version of this constraint has already been published in [START_REF] Jörges | Model Driven Design of Reliable Robot Control Programs Using the jABC[END_REF], but during the further evolution of Genesys, it has been refined by adding the special cases of logging and the successful (error-free) code generation.

< error > true ∨ GenerationSuccessful ∨ GenerationFailed ∨ Log
Example (2) is a constraint which is not only applicable to code generators, but to all kinds of executable SLGs. It refers to a jABC feature that ensures the integrity of SLGs, even if required SIBs cannot be loaded (e.g. because a SIB has been deleted, or the current user simply does not have access to a SIB). In such a case jABC replaces the affected SIBs by so-called proxy SIBs. Via these placeholders, the user is able to do all modeling work as usual: the affected SLGs can be loaded, and the parameters and branches of proxy SIBs can be edited. However, when it comes to the code generation for an SLG, it must not contain any proxy SIBs because they lack the required execution code. To ensure that no such placeholders are contained in an SLG, constraint 2 uses GEAR macros to check two cases:

• SIB.isReplaced is true if a SIB has been automatically replaced by a proxy SIB.

• SIB.isP roxySib is true if a user misapplied a proxy SIB for modeling (which was technically possible in earlier versions of jABC).

The constraint demands that these two cases do not occur in all SLGs by using the specification pattern "Absence" with the scope "globally" [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification[END_REF]. This pattern means "P has to be false globally" and translates to the CTL formula AG(!P).

The formula graphs 3 and 4 in Fig. 6 exemplify the use of hierarchy when modeling constraints with the FormulaBuilder. Formula graph 4 corresponds to the formula SIB.isStartSib ∧ [ ]f alse, which is true for any start SIBs without any predecessors (usually applies to the very first SIB of an SLG hierarchy). In this formula, SIB.isStartSib again is a GEAR macro, while [ ] (resp. BOXB in formula graph 4) is the backward variant of the box operator. By using jABC's hierarchy feature, this formula graph is embedded into formula graph 3 in order to produce a new constraint.

The constraint composed of graphs 3 and 4 demands the use of a SIB called InitCodeGeneration, which is obligatory for all code generators. This SIB initializes several data structures and helper functionality essential for any code generation process, e.g. for impeding the multiple generation of identifier names (which usually leads to uncompilable code). For this purpose, the constraint uses SIB.class == . * InitCodeGeneration which is true for all SIBs whose class name matches the regular expression . * InitCodeGeneration. Furthermore, another specification pattern is used: "Existence" with scope "globally" means "P has to become true globally" and translates to AF (P). Via the embedded formula graph 4, the constraint additionally demands that InitCodeGeneration is the very first SIB of any code generator. When comparing the formula graphs 3 and 4 in Fig. 6 with the corresponding textual formula given above in (3 & 4), the benefit of the graphical representation becomes apparent. Due to the structural reuse that is typical for directed acyclic graphs and the hierarchy features, formula graph representations are particularly beneficial for defining increasingly complex formulas.

Order Constraints

Fig. 7 shows two examples from the actionOrder category, which represent the following constraints:

(1) After it is initialized, the generator either finishes successfully or fails:

(GenerationSuccessful ∨ GenerationFailed) respondsto globally Initialization

(2) The extrusion phase has to be executed before the generation terminates:

Extrusion precedes globally GenerationTerminated Constraint (1) uses the specification pattern "Response" with scope "globally" to specify the allowed outcomes of a generation run, once the code generator has been initialized. This pattern means "S globally has to respond to P" and translates to AG(P ⇒ AF (S)).

The constraint in example (2) is concerned with the order of phases in the generation run. It assures that the extrusion phase, which contains the processing of the input models and the code generation itself, is definitely executed before the generation is terminated. Again, a specification pattern is used: It is called "Response" with scope "globally", means "S globally has to precede P" and translates to A[¬P W U S].

Deriving Patterns & Composing Constraints

As many requirements for code generators lead to very similar formulas, new patterns can often be derived from structural similarities of the corresponding formula graphs.

For instance, imagine a constraint that should ensure the complete treatment of all the constituents of the SLGs that serve as an input for a code generator. A corresponding constraint must not only check that for every input SLG all contained SIBs are guaranteed to be processed, but also the SIB's parameters and branches, etc. It appeared that all these checks follow a similar new pattern, which we call Handle By. It is partly based upon "Precedence" and thus belongs to Dwyer et. al.'s class of "Order patterns". Basically, the new pattern adds to "Precedence" the possibility to describe conditional cause-effect relationships. In the description style of [START_REF] Dwyer | Patterns in Property Specifications for Finite-State Verification[END_REF], the pattern's intent is: Definition 2 (Intent of "Handle By"). "To describe cause-effect relationships between a pair of events/ states on certain conditions. Under certain conditions, an occurrence of the first, the cause, must be handled by an occurrence of the second, the effect."

In its current version, the pattern only exists with the scope "before", as other scopes were not required yet. In textual form, this version of the pattern is to be read as "Handle every A by P before Q". The formula graph in Fig. 8 shows the pattern, which is basically modeled as an incomplete formula graph with:

• one model branch P (indicated in Fig. 8 by a dotted arrow) as well as • three model parameters A, Q and conditions.

As A and Q are currently realized as parameters of the pattern, these slots can only be filled by atomic propositions, not by entire formulas (as it is the case with P). This basically was an intentional and pragmatic decision, as in all our scenarios, A and Q had always been atomic propositions. Nevertheless the pattern could be quickly and easily adjusted for supporting formulas in the slots A and Q. conditions provides a list of branch names that represent the conditions under which A will be handled by P.

To use the pattern, it can be simply embedded into a formula graph using jABC's hierarchy feature, as depicted by the left graph in Fig. 9. The nodes labelled 1 to 3 of this graphs use the "Handle By" pattern in the before scope. For instance, node 1 instantiates the pattern with:

• the atomic proposition NextModel as the cause, • node 2 as the effect, • "next" as the branch condition, and • the atomic proposition GenerationTerminated for the "before" scope.

Besides using hierarchy to simplify constraints via the use and creation of patterns, constraints can be combined with and embedded into each other to capture big requirements of whole SLG hierarchies. All code generators in Genesys are hierarchical SLGs, with a typical code generator model forming a hierarchy of around 20 SLGs, each of them containing around 20 SIB. This means that a typical code generator consists of about 400 SIBs.

An example of a composite constraint is depicted in Fig. 9. It elaborates on the idea outlined above: checking a complete processing of all SLGs that serve as an input to a code generator. This should ensure that no information is lost or forgotten when generating code from a hierarchical SLG. The constraint focuses on the generation of code for SIB parameters and contains the following requirements:

(1) Handle every input SLG before the generation terminates, by (2) handling every SIB before handling the next SLG, by (3) handling every SIB parameter before handling the next SIB, by (4) generating code for either a "normal" SIB parameter or for a model parameter before handling the next SIB parameter.

As a textual formula, this constraint would translate to (again in a syntax close to GEAR's input syntax):

AG(NextModel ⇒ [next]( AG(NextSIB ⇒ [next]( AG(NextSIBParameter ⇒ [next]( A[!NextSIBParameter W U (GenerateSIBParameter ∨ GenerateModelParameter)] )) ∧ A[¬NextSIB W U NextSIBParameter] )) ∧ A[¬NextModel W U NextSIB] )) ∧ A[¬GenerationTerminated W U NextModel]
This formula certainly is not very intuitive, and it is rather laborious for a user to create and understand it. When modeling the constraint explicitly as a formula graph, as depicted on the right side of Fig. 9, it gets much more concise due to the consequent use of jABC's hierarchy feature, and of specification patterns like "Precedence". Furthermore, if patterns like "Handle By" can be identified and created in the fashion exemplified above, the constraints become simple, revealing the true intent of the designer.

By combining and embedding constraints this way, Genesys' constraint library for code generators grows rapidly, and the constraints tend to be more and more concise and effective.

Related Work

There are various approaches that aim at assuring the reliability of automatic code generation. A "verifying compiler", as proposed by Tony Hoare and Jay Misra in their grand challenge [START_REF] Hoare | Verified Software: Theories, Tools, Experiments. Vision of a Grand Challenge Project[END_REF][START_REF] Hoare | The Verifying Compiler: A Grand Challenge for Computing Research[END_REF], is one possible solution to achieve this goal. According to this approach, the compiler is able to determine the correctness of the problem by using additional information, like e.g. assertions or annotations, in the source code.

A lot of research has been done on this, e.g. taking the form of proof-carrying code [Nec97, App01] or evidence-based approaches [START_REF] Denney | Extending Source Code Generators for Evidence-based Software Certification[END_REF]. Other work aims at verifying the compiler itself, like e.g. the Verifix project [START_REF] Goos | Verification of Compilers[END_REF], or at validating the translation especially for optimizing compilers [START_REF] Necula | Translation Validation for an Optimizing Compiler[END_REF]. In contrast to these rather analytical techniques, constructive approaches postulate a more systematic development process, e.g. based on the adoption of accepted standards [START_REF] Stürmer | Overview of existing safeguarding techniques for automatically generated code[END_REF] or the generation of code from specifications [START_REF] Coglio | A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets[END_REF].

All these approaches have in common that they work more or less on the source code level. As all code generators in the Genesys framework are modeled as SLGs, the verification approach presented in this article is applied on the design or process level, which is one of the key ideas of the XMDD paradigm. This allows us to formulate constraints which are not only applicable to one code generator, but to whole families of code generators.

Our graphical way of constructing constraints or rules is also comparable to several related research projects which are concerned with simplifying the specification of such properties. For instance, the Propel-System [SACO02] tries to increase the precision of Dwyer et. al.'s specification patterns by offering additional options to cover alternatives in the behavior that is to be specified. The patterns are presented by means of two complementary views: the first is based on a restricted subset of natural language called DNL (disciplined natural language), the other uses finite-state automata for visualization. As the formula graphs used in our solution are based on SLGs, we profit from the powerful hierarchy mechanisms that allow us to easily derive new, more precise and even domain-specific patterns.

Beside the specification pattern system, there are also other approaches that try to simplify the specification of formulas. Graphical Interval Logic (GIL) [DKM + 94] provides a graphical notation which can be used to model temporal properties of a system. Here intervals serve for the definition of contexts in which particular properties hold. Other projects like e.g. Prosper [START_REF] Holt | Formal verification with natural language specifications: guidelines, experiments and lessons so far[END_REF] or Attempto Controlled English [START_REF] Fuchs | Attempto controlled english -not just another logic specification language[END_REF] try to employ restricted ("controlled") versions of natural language for the specification of properties. Our approach uses the specification patterns as a fundament, because due to their parameterizablity and reusability they fit well into the concept of SIBs and are suitable as components of SLGs.

Conclusion and Future Work

We have presented our approach to the model checking-based verification of code generators in Genesys. Genesys is a framework for the high-level construction of code generators along the lines of the Extreme Model-Driven Development (XMDD) paradigm. In our experience, the development of code generators with Genesys boils down to re-instantiating patterns or slightly modifying the graphical process model. These activities are strongly supported by our verification facilities, which help leveraging the increasing body of domain knowledge in terms of constraints, features and patterns during code generator construction. We have shown how we support the build-up of this body of knowledge along the construction and structuring of a complex constraint, which enforces a certain notion of completeness of the code generation process.

Currently, we are also investigating data flow analysis via model checking (DFA-MC [START_REF] Steffen | Data Flow Analysis as Model Checking[END_REF][START_REF] Lamprecht | Data-Flow Analysis as Model Checking Within the jABC[END_REF]) as a technique for further increasing the quality of our code generators. Interestingly, DFA-MC is applicable for us on the component level as well as on the process level. As our components, the SIBs, are Java classes, we can directly use DFA-MC on them, just as described in [START_REF] Lamprecht | Data-Flow Analysis as Model Checking Within the jABC[END_REF]. At the process level, we need to annotate the contained components with data flow information to be able to perform such analyses. This is part of the corresponding domain modeling, which typically requires manual effort, but we also envisage the support by further analyses or by employing a systematic way of incorporating service-level agreements.

To complement our verification facilities, we also envision a more seamless combination of code generation and testing. It is e.g. imaginable to attach test cases (themselves modeled as SLGs [NSM + 01]) to the SLGs of a modeled application. Along with the source code for the application, the code generators could then also translate the test cases to source code for a common testing framework like e.g. JUnit [START_REF]Object Mentor[END_REF] as part of the quality management process -again modeled with the jABC framework.

Fig. 1 .

 1 Fig. 1. XMDD with jABC & Genesys

Fig. 2 .

 2 Fig. 2. The user interface of jABC

Fig. 3 .

 3 Fig. 3. A hierarchical code generator SLG (shared by all Extruders)

Fig. 4 .

 4 Fig. 4. Checking local constraints with the LocalChecker

Fig. 5 .

 5 Fig. 5. Verifying the Java Class Extruder with GEAR & the FormulaBuilder

( 2 )

 2 No proxy SIBs: absence globally (SIB.isP roxySib) ∧ absence globally (SIB.isReplaced) (3 & 4) SIB InitCodeGeneration is used and is a start SIB without any predecessors: existence globally (SIB.class == . * InitCodeGeneration) ∧ ((SIB.class == . * InitCodeGeneration) ⇒ (SIB.isStartSib ∧ [ ]f alse))

Fig. 6 .

 6 Fig. 6. Three constraints from the category actionOccurrence: (1) "All errors are handled or at least logged, otherwise the generation fails or finishes successfully.", (2) "No proxy SIBs.", (3) & (4) SIB InitCodeGeneration is used and is a start SIB without ay predecessors.

Fig. 7 .

 7 Fig.7. Two constraints from the category actionOrder: (1) "After it is initialized, the generator either finishes successfully or fails.", (2) "The extrusion phase has to be executed before the generation terminates."

Fig. 8 .

 8 Fig. 8. The "Handle By" pattern with scope "before", meaning "Handle every A by P before Q".

Fig. 9 .

 9 Fig. 9. A constraint checking for the complete handling of input SLGs, using the new "Handle By" pattern


Metod Saniga
email: msaniga@astro.sk

Péter Lévay
email: levay@neumann.phy.bme.hu

Mermin's Pentagram as an Ovoid of PG(3, 2)

Keywords:

Mermin's pentagram, a specific set of ten three-qubit observables arranged in quadruples of pairwise commuting ones into five edges of a pentagram and used to provide a very simple proof of the Kochen-Specker theorem, is shown to be isomorphic to an ovoid (elliptic quadric) of the three-dimensional projective space of order two, PG(3, 2). This demonstration employs properties of the real three-qubit Pauli group embodied in the geometry of the symplectic polar space W (5, 2) and rests on the facts that: 1) the four observables/operators on any of the five edges of the pentagram can be viewed as points of an affine plane of order two, 2) all the ten observables lie on a hyperbolic quadric of the five-dimensional projective space of order two, PG(5, 2), and 3) that the points of this quadric are in a well-known bijective correspondence with the lines of PG(3, 2).

Introduction

In 1993, Mermin [1] proposed two ingenious and remarkably simple geometrical proofs of the Kochen-Specker theorem. The first one, which became known as Mermin's (magic) square, employs a set of nine elements/observables of the generalized Pauli group of two-qubits. These nine observables are placed at the vertices of a 3 × 3 grid and form six sets of three pairwise commuting elements, lying along three horizontal and three vertical lines, each observable thus pertaining to two such sets. The observables are selected in such a way that the product of their triples in five of the six sets is +I, whilst in the remaining set it is -I, I being the identity matrix. The second proof, known as Mermin's (magic) pentagram, uses a set of ten elements of the three-qubit Pauli group. Here, the ten observables form five sets of four mutually commuting elements placed along the five edges of a pentagram. Again, each observable belongs to two such sets ("contexts") and the product of fours in any given sets is +I except for one where it yields -I.

Soon after the properties of N-qubit Pauli groups were found to be fully encoded in the geometry of the symplectic polar spaces of rank N and order two, W (2N -1, 2) [2,3,4], the Mermin (magic) square could readily be ascribed a neat finite geometrical meaning, namely as: a special kind of geometric hyperplane of W (3, 2) [2,3], a hyperbolic quadric in PG(3, 2) [4], or a projective line over the direct product of two smallest Galois fields, P 1 (GF (2) × GF (2)) [5]. These last findings repeatedly turned out to be of great physical importance, for example, in revealing a fascinating finite-geometrical meaning of the E 6(6) -symmetric black hole entropy formula of D = 5 supergravity theories [6]. In the present paper, employing basic properties of the finite symplectic polar space behind the three-qubit Pauli group, we shall show that the structure of the Mermin pentagrammatic configuration can similarly be recast in terms of another well-known object of finite geometry.

2 Mermin's Pentagram, Affine Plane of Order Two, the Klein Quadric, the Klein Correspondence and an Ovoid of PG(3, 2)

Our starting point is a particular copy of the Mermin pentagram depicted in Figure 1, left; here I is the 8 × 8 identity matrix, X ≡ σ x , Z ≡ σ z , and, e. g., ZZZ is a shorthand for Z ⊗ Z ⊗ Z. The set of ten three-qubit operators we adopted is, however, not that of Mermin [1], but that of Aravind [START_REF] Aravind | Mermin's Pentagram and Bell's Theorem[END_REF], who was motivated by the paper by Kernaghan and Peres [START_REF] Kernaghan | [END_REF]. The reason is that all the ten matrices are real and can thus be viewed as a subset of the real three-qubit Pauli group. In order to "decipher" the structure of our Mermin's pentagram one has to invoke certain aspects of the finite geometric interpretation of the real three qubit Pauli group [2,3,4]. Omitting the identity and disregarding signs, 63 elements of this group correspond to 63 points of the symplectic polar space W (5, 2), and maximal subsets of pairwise commuting elements of the group have their counterparts in maximal totally isotropic subspaces of W (5, 2), which are Fano planes. As each Fano plane has seven points, any maximal subset of mutually commuting operators is of cardinality seven. Each edge from our Mermin's pentagram, obviously, selects from its ambient Fano plane only four points. There are two possibilities for such a selection; either no three of these four points are collinear (Figure 2), or three of them lie on a line in the corresponding Fano plane (Figure 3). The second possibility can, however, be readily disregarded as the four observables on any edge have obviously the same footing. This implies that each edge of the pentagram is a copy of the affine plane of order two and the pentagram framework can be reformulated as five affine planes of order two sharing pairwise a single point, no three being on the same point -see Figure 1, right. Next we employ the fact that we are dealing with the real three-qubit Pauli group. In such a case [4] the structure of the symplectic polar space W (5, 2) is refined in terms of the orthogonal polar space Q + (5, 2) (which is nothing but the famous Klein quadric), the points of which correspond to the symmetric operators/elements of the group. As all ten observables of our pentagram are symmetric, they must lie on Q + (5, 2). Now, the generators of Q + (5, 2) (i. e., maximal subspaces fully lying on Q + (5, 2)) are Fano planes and there are two systems of them, each having 15 members. Any two distinct planes from the same system share a point, whilst two planes from different systems are either disjoint, or have a line in common (see, e. g., [START_REF] Hirschfeld | Finite Projective Spaces of Three Dimensions[END_REF][START_REF] Conwell | [END_REF]). It then follows that our five affine planes must all originate from Fano planes of the same system. As a final step, we employ the famous Klein correspondence between the points of the Klein quadric Q + (5, 2) and the lines of PG(3, 2) (see, e. g., Table 15. 10 of [START_REF] Hirschfeld | Finite Projective Spaces of Three Dimensions[END_REF] for more details). Under this correspondence, the seven points in a plane of one system of Q + (5, 2) correspond to the seven lines through a point of PG (3,2), and those of a plane of the other system to the seven lines lying in a plane of PG (3,2); an affine plane of order two lying on Q + (5, 2) will then have for its PG(3, 2)-image either four lines through a point, no three coplanar, or four lines in a plane, no three concurrent. Adopting the former view, we thus find that the PG(5, 2)-configuration depicted in Figure 1, right, has for its PG(3, 2)-counterpart the set of five points, no three collinear and no four lying in the same plane, that is, a copy of an ovoid (or, elliptic quadric) (see, e. g., [START_REF] Hirschfeld | Finite Projective Spaces of Three Dimensions[END_REF]). The ten three-qubit Pauli matrices of the pentagram are thus represented by ten lines joining the five points of the ovoid in pairs -as illustrated in Figure 4.

We started this section by the observation that the four observables sharing an edge of the pentagram do not represent a maximal commuting set in the corresponding three-qubit Pauli group. We also stressed that any such maximal set consists of seven elements carried by a Fano plane of W (5, 2). It is, therefore, instructive to see explicitly the projective closures of the edges (up to signs): {ZZI, ZIZ, IZZ} (for green edge), {XXI, XIZ, IXZ} (for blue edge), {XIX, IZX, XZI} (for violet edge), {IXX, ZXI, ZIX} (for yellow edge), {IY Y, Y IY, Y Y I} (for red edge), where Y ≡ iσ y . One can readily check that, up to a sign, the product of each of the five triples of observables is the identity matrix and so each of them represents indeed a line in the associated Fano plane (which is highlighted in Figure 2, left, by three big bullets). One further notes that only the observables of the red-edge projective closure contain the matrix Y , which reflects the fact that this edge stands on a different footing that the other four.

Conclusion

We have shown that the Mermin pentagrammatic framework of ten three-qubit observables, which furnishes a very economic and elegant proof of the Kochen-Specker theorem, can be viewed as a distinguished object of finite geometry, namely an ovoid (elliptic) quadric of PG (3,2); the five edges of the pentagram correspond to the five points of the ovoid and its ten vertices/observables are represented by the lines joining pairs of points of the ovoid. This finding may serve as another justification of our firm belief that all important sets of operators/observables associated with finite-dimensional Hilbert spaces are underlaid by notable objects of finite geometry. In the light of this paper, a particularly interesting and challenging task would be to look for higher-rank analogues of Mermin's configuration(s). Already the next case in the hierarchy, N = 4, deserves serious attention. This is mainly because an associated hyperbolic quadric Q + (7, 2), the locus of symmetric elements of the four-qubit Pauli group, is unusual in that it admits a graph automorphism of order three known as a triality that swaps its points and two systems of generators, and preserves the set of totally singular lines (see, e. g., [11]).

Figure 1 :

 1 Figure 1: Left: -An illustration of the Mermin pentagram. The four three-qubit observables along any edge are pairwise commuting; the product of those along the horizontal (red) edge is -I, while those along any other edge multiply to +I. Right: -A picture of the finite geometric configuration behind the Mermin pentagram: the five edges of the pentagram correspond to five copies of the affine plane of order two, sharing pairwise a single point.

Figure 2 :

 2 Figure 2: An illustration of the case (left) where no three of the four observables (represented by empty circles) pertaining to an edge are collinear in the associated Fano plane; they form an affine plane of order two (right).

Figure 3 :

 3 Figure 3: An illustration of a hypothetical case where three of the four observables would lie on a line of the Fano plane.

Figure 4 :

 4 Figure 4: The PG(3, 2)-image of the Mermin pentagram under the Klein correspondence.The edges of the pentagram correspond to the points of an ovoid/elliptic quadric, and its ten observables map into the lines joining the points in pairs.

Acknowledgement

This work was partially supported by the VEGA grant agency projects 2/0092/09 and 2/0098/10. We are extremely grateful to our friend Petr Pracna for electronic versions of the figures.