Metadata-Version: 1.1
Name: STLInspector
Version: 1.1.4
Summary: Systematic validation of Signal Temporal Logic (STL) specifications against informal textual requirements.
Home-page: https://github.com/STLInspector/STLInspector
Author: Eva Charlotte Mayer, Hendrik Roehm
Author-email: eva-charlotte.mayer@posteo.de, git@roehm.ws
License: Apache License 2.0
Description: STLInspector
        ============
        
        Systematic validation of Signal Temporal Logic (STL) specifications
        against informal textual requirements.
        
        --------------
        
        The goal of
        `STLInspector <http://github.com/STLInspector/STLInspector>`__ is to
        identify typical faults that occur in the process of formalizing
        requirements by mutating a candidate specification.
        `STLInspector <http://github.com/STLInspector/STLInspector>`__ computes
        a series of representative signals that enables a requirements engineer
        to validate a candidate specification against all its mutated variants,
        thus achieving full mutation coverage. By visual inspection of the
        signals via a web-based GUI, an engineer can obtain high confidence in
        the correctness of the formalization - even if she is not familiar with
        STL. `STLInspector <http://github.com/STLInspector/STLInspector>`__
        makes the assessment of formal specifications accessible to a wide range
        of developers, hence contributes to leveraging the use of formal
        specifications and computer-aided verification in practice.
        
        Installation
        ------------
        
        `STLInspector <http://github.com/STLInspector/STLInspector>`__ depends
        on `Python 2 <http://www.python.org>`__, `ANTLR
        v4 <http://github.com/antlr/antlr4>`__, the theorem prover
        `Z3 <http://github.com/Z3Prover/z3>`__ with Python bindings and the
        Python packages `Flask <http://flask.pocoo.org/>`__ and
        `Flask-Assets <https://flask-assets.readthedocs.io/en/latest/>`__.
        Additionally, the GUI depends on
        `Bootstrap <http://getbootstrap.com/>`__,
        `jQuery <https://jquery.com/>`__, `jQuery UI <https://jqueryui.com/>`__,
        `Chart.js <http://www.chartjs.org/>`__, and
        `handlebars <http://handlebarsjs.com/>`__.
        
        Install the Python 2 >= 2.7.9 using your package manager or download it
        from http://www.python.org/downloads. This also provides the Python
        package manager pip.
        `STLInspector <http://github.com/STLInspector/STLInspector>`__ is
        provided as an `python
        package <https://pypi.python.org/pypi/STLInspector>`__ and can be
        installed using pip:
        
        .. code:: bash
        
           pip install STLInspector
        
        Note that the required javascript frameworks are not installed locally,
        but loaded over an internet connection. This comes with the restriction
        that you can used the GUI with an internet connection only. Due to
        safety reasons, network access to the GUI is forbidden and the GUI is
        only available via localhost.
        
        Tutorial
        --------
        
        This is a tutorial that demonstrates how to use
        `STLInspector <http://github.com/STLInspector/STLInspector>`__. It shows
        the standard workflow of the program with an example requirement. For a
        deeper understanding consider reading the
        `documentation <https://github.com/STLInspector/STLInspector/tree/master/STLInspector/doc>`__.
        
        1.  Start the server by executing ``stlinspector .``.
        2.  Open a browser and go to http://localhost:5000.
        3.  Press the *new requirements project* button, input the title
            *tutorial requirements project* and press the *add* button. The
            project overview opens.
        4.  In the *textual requirements* block press the *edit* button and
            input:
        
               The velocity should be higher than 5km/h from second 1 to second
               3.
        
        5.  In the *current STL candidate* block press the *edit* button and
            input:
        
               F[1,3] velocity > 5
        
        6.  Under *visual inspection results* replace *Name* with *Test User*
            and press *new visual inspection*.
        7.  The textual requirement and a test signal is shown. Evaluate the
            textual requirement on the test signal and press the *yes* or *no*
            button. Do this until no test signals are shown any more. Then press
            *go back to project overview*.
        8.  To see the evaluation results, press the *show results* button.
            Since in our example the STL candidate is wrong, some of your
            evaluation results should differ from the STL candidate results.
        9.  Change the STL candidate to:
        
               G[1,3] velocity > 5
        
        10. Redo the visual inspection on the new STL candidate.
        11. You should not get conflicting evaluation results for the STL
            candidate now.
        12. Press the save button and the project is saved to
            ``tutorial_requirements_project.stlinspector`` in the current
            directory. Congratulations, you validated the STL candidate against
            the textual requirement!
        
        Documentation
        -------------
        
        Further information can be found in the
        `documentation <https://github.com/STLInspector/STLInspector/tree/master/STLInspector/doc>`__
        that details the use of the web-based GUI, the parser and the mutation
        operators. The GUI provides a html version of the documentation.
        
        Contributing
        ------------
        
        We greatly appreciate fixes and new features for
        `STLInspector <http://github.com/STLInspector/STLInspector>`__. All
        contributions to this project should be sent as pull requests on github.
        `STLInspector <http://github.com/STLInspector/STLInspector>`__ uses
        *semantic versioning* as described in
        `packaging.python.org <https://packaging.python.org/distributing/#choosing-a-versioning-scheme>`__.
        Please run test suite ``python setup.py test`` before requesting a pull.
        
        Licence
        -------
        
        `STLInspector <http://github.com/STLInspector/STLInspector>`__ is
        released under the `Apache Licence
        2.0 <https://github.com/STLInspector/STLInspector/blob/master/LICENSE>`__.
        
Platform: UNKNOWN
Classifier: Development Status :: 4 - Beta
Classifier: Environment :: Web Environment
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: Apache Software License
Classifier: Programming Language :: Python :: 2.7
Classifier: Topic :: Scientific/Engineering
Classifier: Topic :: Software Development
