BPjs: A JavaScript-based Behavioral Programming Runtime.

This repository contains a javascript-based BP library.

License

• BPjs is open sourced under the MIT license. If you use it in a system, please provide a link to this page somewhere in the documentation/system about section.
• BPjs uses the Mozilla Rhino JavaScript engine. Project page and source code can be found here.

Academic Citation

If you use BPjs in an academic work, please consider citing it as:

Bar-Sinai M., Weiss G. (2021) Verification of Liveness and Safety Properties of Behavioral Programs Using BPjs. In: Margaria T., Steffen B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends. ISoLA 2020. Lecture Notes in Computer Science, vol 12479. Springer, Cham. https://doi.org/10.1007/978-3-030-83723-5_14

bibtex

---

Getting BPjs

• For Maven projects: Add BPjs as dependency. Note that the version number changes.

<dependencies>
    ...
    <dependency>
        <groupId>com.github.bthink-bgu</groupId>
        <artifactId>BPjs</artifactId>
        <version>0.12.2</version>
    </dependency>
    ...
</dependencies>

• Clone, fork, or download the starting project.
• Download the .jar files directly from Maven Central.
• The project's Google group

Documentation

• Devoxx Belgium 2018 talk introducing Behavioral Programming and BPjs.
• Presentations: Introduction Deeper dive
• Tutorial and Reference
• API Javadocs

Change Log for the BPjs Library.

2022-07

• ⬆️ ✨ Moved to Rhino 1.7.14. This means many new features, including template strings and better Java interoperability. See full list on Mozilla's site. (#186).
  • 〽️ Refactored internals fo better fit the new Rhino version. We now have a proper context factory, as well as try-with-resources on all context invocations.
• 〽️ BProgramRunnerListener defautls to ignore errors during BProgram execution, instead of printing the details to stderr. This behavior remains in BProgramRunnerListenerAdapter, where it makes more sense. Of course, client code can override these methods. (#191).
• ⬆️ Printing problematic b-thread's name during serialization errors (#169).
• ✨ Custom serialization for the common and non-serializable java.util.Optional and JavaScript's Set(). (#189)
  • This is a basis for custom serializations in general, we now have an initial mechanism in place.
• ⬆️ Improved wrapping of Java objects as they come to JavaScript: Java strings are now treated as native JS strings, so using the === operator works as expected. (#104).
• 🐛 Verification stops on ECMAScript errors, instead of hanging (#49).
• 🐛 Improved error reporting when trying to sync outside of a b-thread (#174).
• ⬆️ Informative error message when requesting a list of events and one of the events is null (#184).
• ⬆️ Logging is turned off by default during verification. Call BPjs.setLogDuringVerification(true) to enable them again (#160).
• ✨ Added local JACOCO code coverage reports.

2022-02 (Including the 1st BP Day Hackathon)

• 〽️ Calling bp.sync from global scope during runtime does not cause an ugly exception anymore (#174). The error is reported to the listeners.
  • Also when making the illegal call from an interrupt handler.
• ⬆️ Improved JavaScript code error detection during analysis
• ⬆️ Improvements to handling nulls in event set arrays (#178).
• ⬆️ Improvements to handling Rhino context in BPjs class (#176).
• ⬆️ Improvements to the MapProxy classes, allowing client code pre-process changes.
• ⬆️ JsEventSet now honors the event set name during equality checks.
• 〽️ BEvent::getDataField data accessors wrap the lower-level getData() (#161).
• 〽️ API improvments on DfcBProgramVerifier (#173).
• 🚮 Consolidated tests for BProgramJsProxy.

2022-01

• ⬆️ Improvements to the BEvent class, to make it better support client Java code.

2021-10

• ✨ Added contribution guidelines (#139).
• ✨ Reference to the (finally) published paper describing the updated BPjs model semantics, w.r.t liveness (#99).

2021-05

• ✨ Client code can change the execution services BPjs uses (#165).
• ✨ bp.log.XXX can be redirected to print streams other than System.out. (#159).
• ⬆️ Documentation updates.
• ⬆️ Improved performance of BTSS equality (#164).
• ⬆️ Removed broken JS code in tests (#153).

2021-02

• ✨ ✨ 🎉 ✨ 🎉 ✨ 🌈 ✨ ✨ ✨ BPjs now uses Rhino's native continuation equality and hash code (#116. Also, 🎉 🌈 ✨.
• ⬆️ Scope and context creations across BPjs have been consolidated to utility methods in a new class called BPjs.
• ⬆️ Event selection strategies that ignore the synchronization statement data field, issue a warning when b-threads put data there (#151).
• ⬆️ Default priorities in PrioritizedBSyncEventSelectionStrategy and PrioritizedBThreadsEventSelectionStrategy can be changed (#115 and PR#147).
• ⬆️ Updated docs.
• ⬆️ BProgram uses an override-able protected method to access its global scope, in case you want to intercept these calls.
• 🐛 Fixed an issue that caused toString for JavaScript objects to crash at certain cases (#145).
• 🐛 Storage consolidation conflicts have proper equals and hashCode.

2021-01

• ✨ BProgramSyncSnapshots are serialized using a single stream, and with the b-program's original scope as a top-level scope ((#126).
• ✨ BThread snapshots do not retain their entry point function after their first sync point. This results in lower memory footprint, and a more efficient de/serialization. These result in improved analysis performance and efficiency.
• ✨ Event sets (and, by inheritance, events) are now composable. So you can write, e.g., bp.Event("A").or(bp.Event("B")).negate() to create an event set that contains all events except A and B.
• ✨ Another easy event set composition/creation added: bp.eventSets gives access to EventSets, with methods such as bp.eventSets.anyOf(...) and bp.eventSets.not(...)
• ⬆️ Logging now allows formatting, using Java's MessageFormat.
• ⬆️ Expressive toString on JavaScript sets (#135).
• ⬆️ Error messages when passing non-events to a synchronization statement are more informative (#131).
• ⬆️ Improved logging consistency (#132).
• ⬆️ Error messages when JS event sets do not return a Boolean are more informative (#138).
• ⬆️ BThread data documentation updated (#134).
• ⬆️ BProgram storage can be updated by the b-program before b-threads run (#129).
• ⬆️ Changes made to the b-program store after the last sync of a b-thread are now applied (#130).
• ⬆️ More tests (logger, JSProxy, ScriptableUtils, OrderedSet, JsEventSet, some event selection strategies).
• 🐛 🎉 JS-semantics are applied for equals and hashCode for b-thread and b-program data (#144).
• 🐛 Fixed the note color issue in the documentation (#137).
• 🐛 Fixed the bench marker.
• 🐛 Fixes a crash when a JS event set predicate returns null instead of a boolean.
• 🚮 Significant cleanup of the b-program I/O area.
• 🚮 Significant cleanup of the event set area. Some methods moved from ComposableEventSet to EventSets.
• 🚮 Some documentation updates and corrections.
• 🚮 Removed extraneous dependencies from pom.xml (#133).

Earlier Changes

Legend:

• 🔄 Change
• ✨ New feature
• 🎉 New feature, but more exciting
• 〽️ Refactor (turns out this sign is called "part alternation mark" and not "weird 'M'", so it fits).
• 🚮 Deprecation
• ⬆️ Upgrade
• 🐛 Bug fix