overturetool / overturetool.github.io Goto Github PK

This action concerns creating a new video that demonstrates the new features of the TEMPO UI technology. Possibly using the Alarm example.

The Japanese references are missing from the bib file used on the web. I was unable to find citations for them.

The page that links to the Overture manuals should link to the newest versions:

http://overturetool.org/documentation/manuals.html

PGL will contact Araki-san to get more information regarding the future plans for VDMTools at KU. Including whether or not they will do further development on the tool.

Investigate how to generate a publication page from a gibtex file.

The idea is to resume work on producing a video on VDM targeting the industry (related to issue #14). The task associated to this action is to consider what the message and content for such a video could be. Afterwards @pglvdm will take an action to create such a video.

High download stats for Overture from Porto indicate that it may be used for a course there. PGL will contact them so to see if there are any opportunities for collaboration.

We need a meeting schedule for 2017. @pglvdm has offered to create one.

https://www.overturetool.org/download/ needs to explain about the change of IDE from Eclipse to VSC and explain about the advantages of the new IDE.

Either directly or in a significant form.

Source: overturetool/overture#705 (comment)

• Jozef Hooman and Marcel Verhoef, [[http://www.marcelverhoef.nl/uploads/Main/festschrift.pdf][Formal Semantics of a VDM Extension for Distributed Embedded Systems]], in D. Dams, U. Hannemann and M. Steffen (eds): W.P. de Roever Festschrift, LNCS 5930, pp 142-161, 2010.
• P. G. Larsen, N. Battle, M. Ferreira, J. S. Fitzgerald, K. Lausdahl, M. Verhoef, [[http://portal.acm.org/citation.cfm?id=1668862.1668864&coll=&dl=GUIDE&idx=J728&part=newsletter&WantType=Newsletters&title=ACM%20SIGSOFT%20Software%20Engineering%20Notes&CFID=://www.google.com/search?hl=da&CFTOKEN=www.google.com/search?hl=da][The Overture Initiative: Integrating Tools]] for VDM ACM SIGSOFT Software Engineering Notes Vol. 35, Issue 1, January 2010.
• J. C. Bicarregui, J. S. Fitzgerald, P. G. Larsen and J. C. P. Woodcock, [[http://deploy-eprints.ecs.soton.ac.uk/160/2/BicarreguiEtAlIdayAuth.pdf][Industrial Practice in Formal Methods: a Review]], In Proc. 16th Intl. Symp. on Formal Methods (FM 2009), Lecture Notes in Computer Science, LNCS 5850, pp. 810-814, Springer, November 2009.
• J. C. P. Woodcock, P. G. Larsen, J. Bicarregui and J. Fitzgerald, [[http://doi.acm.org/10.1145/1592434.1592436][Formal methods: Practice and Experience]], ACM Computing Surveys 41(4), 2009, pp. 1-36. DOI 10.1145/1592434.1592436. [[http://deploy-eprints.ecs.soton.ac.uk/161/2/fmsurvey[1].pdf][Authors' draft]]
• K. Lausdahl and H. K. Lintrup and P. G. Larsen, Connecting UML and VDM++ with Open Tool Support, in A. Cavalcanti and D. Dams (Eds.), [[http://www.springer.com/computer/programming/book/978-3-642-05088-6][FM 2009: Formal Methods, Procs. Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009]], LNCS 5850, Springer 2009.
• P. G. Larsen, J. S. Fitzgerald and S. Wolff, [[http://www.ijsi.org/IJSI/ch/reader/view_abstract.aspx?file_no=305&flag=1][Methods for the Development of Distributed Real-Time Embedded Systems using VDM]], International Journal of Software and Informatics, 3(2-3),pp. 305-343, 2009. (Previously [[http://www.cs.ncl.ac.uk/publications/trs/papers/1164.pdf][CS-TR 1164]], School of Computing Science, Newcastle University)
• Taro Kurita, Yasumasa Nakatsugawa. [[http://www.ijsi.org/IJSI/ch/reader/view_abstract.aspx?file_no=273&flag=1][The Application of VDM to the Industrial Development of Firmware for a Smart Card IC Chip]]. International Journal of Software and Informatics, 2009,3(2-3), pp. 343-355, 2009
• P. G. Larsen, J. S. Fitzgerald and S. Riddle. [[http://www.springerlink.com/content/y2361818q6l4gwg6/][Practice-oriented courses in formal methods using VDM++]], Formal Aspects of Computing 21(3), Springer-Verlag, 2009 DOI 10.1007/s00165-008-0068-5
• M. Verhoef, [[http://www.marcelverhoef.nl/pmwiki.php?n=Main.PhdThesis][Modeling and Validating Distributed Embedded Real-Time Systems]], !PhD Thesis, Radboud University Nijmegen, 21 January 2009.
• J. S. Fitzgerald, P. G. Larsen and M. Verhoef, Vienna Development Method, in B. Wah (ed.), Wiley Encyclopedia of Computer Science and Engineering, John Wiley & Sons. ISBN 0471383937, September 2008.
• J. S. Fitzgerald, J. W. Bryans, D. Greathead, C. B. Jones and R. Payne, [[http://www.bcs.org/server.php?show=conWebDoc.18550][Animation-based Validation of a Formal Model of Dynamic Virtual Organisations]], in P. Boca, J. P. Bowen and P. G. Larsen (eds.) Proc. BCS-FACS Workshop on Formal Methods in Industry, Electronic Workshops in Computing, The British Computer Society, 2008.
• John Fitzgerald, Peter Gorm Larsen and Shin Sahara, VDMTools: advances in support for formal modeling in VDM, ACM SIGPLAN Notices 43(2), February 2008. (Previously Technical Report [[http://www.cs.ncl.ac.uk/publications/trs/papers/1057.pdf][CS-TR-1057]], School of Computing Science, Newcastle University)
• P. G. Larsen and J. S. Fitzgerald. [[http://www.bcs.org/server.php?show=conWebDoc.18557][Recent Industrial Applications of VDM in Japan]], in P. Boca, J. P. Bowen and P. G. Larsen (eds.) Proc. BCS-FACS Workshop on Formal Methods in Industry, Electronic Workshops in Computing, The British Computer Society, 2008.
• Hugo Daniel Macedo, Peter Gorm Larsen and John Fitzgerald, Incremental Development of a Distributed Real-Time Model of A Cardiac Pacing System using VDM, in Jorge Cuellar and Tom Maibaum (Eds.), FM 2008: Formal Methods, 15th International Symposium on Formal Methods, Turku, Finland, May 26-30, 2008, Lecture Notes in Computer Science Vol. 5014, ISBN: 9783540682356, May 2008 (Previously Technical Report [[http://www.cs.ncl.ac.uk/publications/trs/papers/1059.pdf][CS-TR-1059]], School of Computing Science, Newcastle University).
• J. S. Fitzgerald and C. B. Jones. The Connection between Two Ways of Reasoning about Partial Functions, The Connection between Two Ways of Reasoning about Partial Functions, Information Processing Letters 107(3-4), pp. 128-132, 2008 (Previous version was Technical Report CS-TR-1044, School of Computing Science, Newcastle University, Aug 2007 [[http://www.cs.ncl.ac.uk/research/pubs/trs/papers/1044.pdf][PDF]]). This paper discusses the relationship between two logics that provide alternative ways of reasoning about partial functions. Theorems in the Logic of Partial Functions using weak equality (the logic on which VDM is based) can be directly translated into First Order Predicate Calculus using existential equality. Translation in the other direction is, in general, more complicated but simplifies pleasingly in many cases. Such results are important if formal methods tool integration is to be done safely.
• Zoe Andrews, John Fitzgerald, Marcel Verhoef. [[http://www.marcelverhoef.nl/uploads/Main/dsn07afv.pdf][Resilience Modelling Through Discrete Event and Continuous Time Co-Simulation]], in Proc. 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (July 2007).
• Marcel Verhoef and Peter Gorm Larsen. Interpreting Distributed System Architectures using VDM++ – A Case Study, in R. Jain, B Stevens, G. Müller (eds.), Proc. 5th Annual Conference on Systems Engineering Research, March 14-16, 2007. ([[%ATTACHURL%/paper119_website.pdf][PDF]]) This provides an overview of the system engineering capabilities in the new extensions of VDM++ enabling the description and analysis of real-time, distributed systems.
• John S. Fitzgerald, Peter Gorm Larsen, Simon Tjell and Marcel Verhoef. Validation Support for Distributed Real-Time Embedded Systems in VDM++, in Proc. 10th IEEE High Assurance Systems Engineering Symposium, Dallas, Texas, Nov. 2007. Revised Version of TR1017, School of Computing Science, Newcastle University, Apr 2007 ([[http://www.cs.ncl.ac.uk/research/pubs/trs/papers/1017.pdf][PDF]]). A new facility is proposed for stating and checking validation conjectures against traces derived from the execution of scenarios on VDM++ models. We describe the implementation of conjectures against execution traces as a formally-defined extension to the existing VDM++ tool set, and show tools to support the visualisation of traces and validation conjecture violations.
• Jeremy W. Bryans and John S. Fitzgerald. Formal Engineering of XACML Access Control Policies in VDM++, in Proc. 9th International Conference on Formal Engineering Methods, Florida Atlantic University, Boca Raton, Florida, USA, November 2007. Also TR 1028, School of Computing Science, Newcastle University, Jan 2007 ([[http://www.cs.ncl.ac.uk/research/pubs/trs/papers/1028.pdf][PDF]]). This provides an introduction to the VDM++ semantics of the eXtensible Access Control Markup Language. Abstractions in the model are potentially very useful in understanding the problems of managing access control in virtual organisations.
• Marcel Verhoef, Peter Gorm Larsen and Jozef Hooman. Modeling and Validating Distributed Embedded Real-Time Systems with VDM++", Springer Verlag Berlin, in FM 2006: Formal Methods, ISBN 3-540-37215-6, August 2006. ([[http://www.springerlink.com/content/5w687059p28t4215/][PDF]]). This provides the semantics and a small case study of new extensions for VDM++ enabling the description and analysis of real-time, distributed systems.
• John Fitzgerald and Peter Gorm Larsen. Triumphs and Challenges for the Industrial Application of Model-Oriented Formal Methods, in T. Margaria, A. Philippou and B. Steffen (eds.), Proc. 2nd Intl. Symp. on Leveraging Applications of Formal Methods, Verification and Validation (!ISoLA 2006), IEEE 2007. Also TR999, School of Computing Science, Newcastle University, Jan 2007 ([[http://www.cs.ncl.ac.uk/research/pubs/trs/papers/999.pdf][PDF]]). This gathers brief details of many of the significant industry applications of VDM and VDM++ in recent years. We compare the tools-based approach of VDM with the vision of "lightweight" formal methods first advocated in the mid-1990s.
• Jeremy Bryans, John Fitzgerald, Cliff Jones, Igor Mozolevsky. Formal Modelling of Dynamic Coalitions, with an Application in Chemical Engineering, in T. Margaria, A. Philippou and B. Steffen (eds.), Proc. 2nd Intl. Symp. on Leveraging Applications of Formal Methods, Verification and Validation (!ISoLA 2006), IEEE 2007. Also TR981, School of Computing Science, Newcastle University, Sep 2006 ([[http://www.cs.ncl.ac.uk/research/pubs/trs/papers/981.pdf][PDF]]). Describes the lightweight use of VDM to map out a space of dynamic coalitions (dynamically changing collections of cooperating agents which share information and work towards a common goal). The models developed are adapted to a real DC in the chemical engineering industry.
• John Fitzgerald, Peter Gorm Larsen and Steve Riddle. Learning by Doing: Practical Courses in Lightweight Formal Methods using VDM++. TR 992, School of Computing Science, Newcastle University, Dec 2006 ([[http://www.cs.ncl.ac.uk/research/pubs/trs/papers/992.pdf][PDF]]). This paper describes the practical approaches to teaching VDM and VDM++ used at Aarhus and Newcastle. It is developed from Peter Gorm Larsen's presentation at the FM06 workshop on Formal Methods Education.
• John Fitzgerald. The Typed Logic of Partial Functions and the Vienna Development Method. in Dines Bjoerner and Martin Henson (eds.) Logics of Specification Languages, Springer Monographs in Theoretical Computer Science (EATCS Series), 2007, pages 427-461. Also TR 984, School of Computing Science, Newcastle University, Oct 2006 ([[http://www.cs.ncl.ac.uk/research/pubs/trs/papers/984.pdf][PDF]]). A technical discussion of the use of the non-Classical Logic of Partial Functions (LPF) to underpin reasoning about VDM models. The paper concentrates on the implementation of the typed form of LPF.
• Jeremy Bryans, John Fitzgerald and Panos Periorellis. Model Based Analysis and Validation of Access Control Policies, TR 976, School of Computing Science, Newcastle University, July 2006 ([[http://www.cs.ncl.ac.uk/research/pubs/trs/papers/976.pdf][PDF]]). A first VDM formalisation of XACML-based access control policies. The model is being developed further and applied to information security for dynamic coalitions.

We need a page that describes the VDM language by:

• first describing the basic VDM of the iso standard, types, functions etc.
• a short section that describes modules
• a short section that describes the addition of ++
• a short section that describes the addition of RT

Created: 6 February 2010 (see [[Net Meeting 41]])

-Owner: Peter Gorm Larsen

-Prepare new materials on how VDM fits into industrial development practice. This is to be aimed at a lay "manager" readership. Contributors: MV, JSF, NB and PGL.

We need, preferably three, Overture release dates for 2020. @pglvdm please post the dates here and then I will go ahead and add the corresponding milestones in the tool repository.

Created: 21 September 2014 (see [[Net Meeting 82]])

-Owner: Ken Pierce

Meet with legal contact about licensing situation

• Go through old core wiki pages and propose new places for them. (Deletion and merging of pages is ok)
• Netmeeting integration into new website: #2
• Dynamic bib page: #3 .

The December 18 meeting (2016) will be moved to January (2017) so more people can attend.

According to the OCP, we must vote over email to change the rules regarding the number of LB members.

PGL will take care of this.

• Make sure Kei Sato is added to the core mailing list (@pglvdm)
• Send mail out to the core group regarding the LB expansion

We need a page that at a high level describes what the core of vdM is all about so you can get an idea about this in 5 min.

Updating the overturetool.org website, by pushing changes to the overturetool.github.io repository, produces the following rather critical warning:

"The page build completed successfully, but returned the following warning for the master branch: The custom domain for your GitHub Pages site is pointed at an outdated IP address. You must update your site’s DNS records if you’d like it to be available via your custom domain. For more information, see https://help.github.com/en/articles/using-a-custom-domain-with-github-pages. For information on troubleshooting Jekyll see: https://help.github.com/articles/troubleshooting-jekyll-builds"

In order to fix this we’d have to go to the company where we purchased the domain and update the DNS settings. However, it is currently unclear who has the power to do this.

We should consider adding the content of the release notes to the downloads page

From overturetool/overture#414 ...

"We have to make a note or FAQ somewhere to assist the user in solving this. It is correct that this is a Java 8 installer problem which sucks in almost all possible ways. It doesn't install the stuff it should be removed more than it is asked for - not a great installer."

New action for PGL to contact MV (cc NB) about the approach to updating the licensing of Fujitsu’s VDMJ, to allow it to be integrated with the Eclipse platform in Overture and other derived tool projects.

Created: 6th July 2014 (see [Net Meeting 80])
Owner: John Fitzgerald

To hold an email/skype discussion about revising the goals for 2020, and the specifics of the semantics, methods&apps and tools pages. Where necessary to include the Language Board.

Clicking on the language manual, the pdf is linked to the master branch of the documentation. Documentation editing is what actually is maintained. To solve it: Change all the links to documentation that mention master. Delete the master documentation branch (minimize possibility of error). Check if pdf can be generated and checked for missing refs in a github action.

Support for annotations has been added
in Overture and VDMJ. Currently, it is only fully supported if you are
using the command-line interface. Unfortunately, we haven't got it to
fully work with the IDE. In particular, annotations that use the
incremental builders to perform parsing and type checking do not
work. The feature itself is documented in the Overture tool manual,
chapter 17:

http://raw.github.com/overturetool/documentation/master/documentation/UserGuideOvertureIDE/OvertureIDEUserGuide.pdf

Essentially annotations (when used via the command-line interface)
work by adding the jars containing the annotations to the classhpath,
e.g:

java -cp "Overture.jar:annotations.jar" org.overture.interpreter.VDMJ -vdmsl -i test.vdmsl

Since we ended up getting stuck with things to try to get it to work
with the IDE, we would like your input.

Below is a list of things we've tried to get annotations to work with
the incremental builders. All of them failed to work. It's mostly a
summary of old emails exchanged between Nick and me. The "quotes" are
either me, Nick or some website.

1. Setting the osgi.dev mode classpath, see
   https://help.eclipse.org/kepler/index.jsp?topic=/org.eclipse.platform.doc.isv/reference/misc/runtime-options.html

2. "set a property -DLIB_LOCATION=/absolute/path/to/lib_dir and use
   external: in your MANIFEST.MF. The you either have to 1) add the
   jars to your Bundle-ClassPath or 2) create their own bundles with
   their Bundle-ClassPath

Bundle-ClassPath:
jars/ast.jar,
jars/parser.jar,
external:$LIB_LOCATION$

Assuming this works the user would still have to update the
Overture.ini to contain something like:

...
-vmargs
-Xmx512m
-Dosgi.requiredJavaVersion=1.8
-DLIB_LOCATION=/usr/local/bin/Overture-2.6.5"

3. "I've tried setting
   -Dosgi.dev=/usr/local/bin/Overture-2.6.5/Annotations.jar in
   Overture.ini, as also suggested in the runtime options help, but
   that didn't work either."

4. "Perhaps the best approach is to wrap the JAR in a plugin/bundle
   and then install that in Overture. I think this might be the
   "cleanest" way to do it but perhaps it's way too much work for the
   user."

"Using the approach suggested in (1) I tried to add the annotations
JAR to Overture's classpath by converting the JAR to an OSGI bundle
and then installing it in Overture (using the "Help -> Install New
Software ..." feature). Although I was able to install the plugin (it
is listed under installed software), Overture did not pick up the
annotations when the model was executed/type-checked. I'm not sure
why. I had expected the .class files to be loaded when the plugin was
installed. But for some reason it only picks up the annotations when I
put the JAR file in the 'lib' folder of the VDM project.

So I was considering whether we can avoid playing around with
Eclipse/OSGI. What if we instead update the Overture core to
dynamically add the JAR file (or the folder that contains it) to the
classpath? The user could still use a property to pass the location of
the JAR (e.g. -DANNOTATIONS_FOLDER or -DANNOTATIONS_JAR).

(1): http://www.vogella.com/tutorials/EclipseJarToPlugin/article.html#convert-jar-files-to-osgi-bundles-with-the-p2-maven-plugin"

5. "I tried to play around with exports as well. Nothing seemed to
   work, unfortunately. I'll try hard coding the path (to begin with)
   when I get a minute."

6. "The only way I can get it to work is by adding the jar to the lib
   folder of the VDM project, which makes the JAR available when the
   interpreter is run, but that doesn't work for incremental
   type-checking. Other than that I can only get it to work via the
   CLI:

java -cp Overture-2.6.5-SNAPSHOT.jar:/home/peter/Desktop/tmp/annotations-pvj.jar org.overture.interpreter.VDMJ -vdmsl -i /home/peter/Downloads/test.vdm

I have tried the following things to get it to work with the IDE (as
described in previous emails):

• installed the annotations JAR as an OSGI bundle and
• updated the ide core and ide builders MANIFEST to include the JAR
  (and export the relevant packages, i.e. org.overture..annotations)

Both attempts failed. Today, I tried new variations of 2) but none of
them worked.

I also tried to pragmatically/dynamically add the JAR using the
approach described in [1] (by hardcoding the path to the JAR) but that
also didn't work.

Lastly, I tried to add the JAR to
/usr/lib/jvm/java-8-oracle/jre/lib/ext and run the CLI but that yields
a NoClassDefFoundError (I'm not sure why)"

7. From Eitienne Brosse: "Now, you have to define what this annotation
   plugin will pass to the other and how it loads the annotation
   jars. Modelio is a Eclipse RCP which can be extended by "deploying"
   modules. These modules are composed of several artefacts including
   jars. These jars are loaded by one specific plugin which passes
   custom Java ClassLoader to the other plugins. We believe that it is
   one possible way to solve your issue. One other possibility, which
   should work (we do not know we have not tried yet), would consist
   in loading your annotations as Eclipse plugins (providing extension
   point(s)) and not "just" jars. This would be cleaner but as I said
   we did not use it in Modelio context."

8. "I've been looking for new ways to avoid meassing around with the
   Eclipse stuff. When doing so I came across this JVM option:

-Xbootclasspath/p:<directories and zip/jar files separated by :>
prepend in front of bootstrap class path

So as far as I understand other people have been using this option to
extend the classpath of the RCP."

"I just tried adding:

-Xbootclasspath/a:/usr/loca/bin/Overture-2.6.5/Annotations.jar

to the Overture.ini, but it doesn't seem to work - neither in the
editor nor the runtime :-("