New PDFs for an Old Ph.D. in formal methods

I completed my Ph.D. in 1997 on The Use of Formal Methods for Safety-Critical Systems. Happy to share the findings, I put copies of thesis online, but whilst LaTeX -> dvi -> postscript may have been routine practice for users of UNIX systems running X Windows, it was not very Web friendly for many others (much as Ghostview is good, it doesn't have such a popular appeal!) Finally I've got round to converting to PDFs and have added them to my PhD page. I tried a few years ago, but my initial attempts generated huge files and I couldn't work out why; fortunately ps2pdf.com's settings were far more reasonable and the entire thesis would almost fit on a 1.4MB floppy disk!

As to the subject matter, I was unable to progress the research as I wished; the small group at Kingston University soon petered out and there were relatively few openings elsewhere, so that's when I moved more towards I.T. from computer science (they are very different activities). In the '90s there were growing hopes that formal methods would gain a more general foothold, but when I glance at FM sites now, it seems their use remains very niche; references to LOTOS, the process algebra that I used to model a communications protocol for medical devices, point to materials that are rather old - the World-wide Environment for Learning LOTOS is indicative of this. There are still research activities, typically in compilation, but overall it's a bit surprising and disappointing. Yet given the greater computing power on tap, particularly cloud computing, perhaps this area may yet develop a lot further...?

Installing MySource Matrix on a Win XP Netbook (for evaluation)

Among the crop of open source content management systems that are deployed at Oxford, I recently had my first encounter with MySource Matrix, developed by Squiz, which is released under GPL. I decided to take a closer look by installing it on a netbook running Windows XP Home, just to have a poke around. The official requirements are a UNIX-like operating system, but this is a Web application, so in principle I think it ought to work, just as I can be confident in installing WordPress or Drupal. This should be the case, even though MySource Matrix is definitely a more substantial proposition in that a default install seems to gives you 'the kitchen sink'. The following is a screenshot after I had created my first page:

As I couldn't find anyone else writing about it I thought I'd share an outline of the process I went through in case others would like to evaluate on this platform. I apologize in advance for not offering any support or follow-ups because I've since moved on/back to other systems for now, so for queries I think the best place would be the support forums.

Requirements

I carried out the installation at the beginning of September 2010, mainly following the steps in the installation guide provided by Squiz. The first thing that I'd stress is that it doesn't support the latest version of PHP. I really should have read the requirements more carefully as I did try 5.3.x and progressed only so far until I hit an issue reported on the forum. Afterwards I dropped back to version 5.2.14.

For the Web server I am running Apache 2.2 and this appears to be the recommended choice for working with the other components.

For the database back-end, MySQL is not supported, but there is a Windows distribution of the freely available PostgreSQL.

Installation

Apache (preliminary): A standard install should be fine as a basis to work with installing PHP and its libraries. For the Matrix config itself, see later.

PostgreSQL: For reference, I used Squiz's page on database installation. I installed Postgres 8.4.x using the Windows easy installer, accepting the defaults. Then for the installation of the Squiz database I used pgadmin, specifically pgAdmin III (v. 1.10.3). From the command line I issued the following commands to create two users: $ createuser -SRDU postgres matrix
$ createuser -SRDU postgres matrix_secondary where -S: NOT a superuser, -R NOT allowed to create roles, -D NOT allowed to create databases, -U connect as username.

Then I created the database: $ createdb -U postgres -O matrix -E SQL_ASCII mysource_matrix, where -O owner, -E encoding. Note that it's important that the right template database is used — template0.

Comment: pgAdmin warns that storing data using the SQL_ASCII encoding means that the encoding is defined for 7 bit characters only. So it is dependent on the Web application to do the conversions (since content served to the Web is typically 8 bit UTF. I wonder if this is an indication of the longevity of the software...?

At some stage, you need to create the PLPGSQL language for Matrix. I did this in pgAdmin once I had run from the command line: C:\PostgreSQL\8.4\bin>createlang.exe -U postgres -d mysource_matrix plpgsql, but for a while I had some difficulties and needed some guidance.

PHP: When installing PHP (I did this via the MSI installer), I did the custom configuration to ensure support for PDO. There are other bits, like SMTP support, that should be included also, but selecting everything is not a good idea because, for instance, it will then expect that an Oracle client is installed. The most immportant of these is the PEAR Package Manager since MySource Matrix depends a lot on the additional PHP libraries that PEAR provides.

I actually did the PEAR installation separate from the main PHP installation, by running the gopear.php script from within a browser and subsequently installing packages through its Web front end. A lot of modules are needed and I'm not sure that my list is complete, but for what it's worth, here is a list of what I've installed so far from the channel pear.php.net: Archive_Tar, Auth_SASL, Cache_Lite, Config 1.10.11, Console_Getopt, HTML_Template_IT, HTTP, HTTP_Client, HTTP_Request, I18N, Image_Canvas, Image_Color, MIME_Type, Mail, Mail_Mime, Mail_Queue, Mail_mimeDecode, Math_BigInteger, Math_Stats, Net_SMTP, Net_Socket, Net_URL, Numbers_Roman, Numbers_Words, PEAR, PEAR_Frontend_Web, Structures_Graph, Text_Diff, Text_Highlighter, XML_HTMLSax, XML_Parser, XML_RPC, XML_Tree. Note that all these are marked 'stable' apart from Image_Canvas (alpha); Numbers_Words and PEAR_Frontend_Web (beta).

Basic Config Settings

With everything in place, I was ready to run the php install scripts. Here I emphasize that the PHP PDO and PDO_PGSQL modules must be installed for this to complete. For step 2, you need to ensure that there is the right access to Postgres. by editing pg_hba.conf to have lines roughly like:

host    all         all         your_local_IP/24          trust

Then at the end of running the script it should report at end: all secondary and tertiary user permissions fixed.

For step 3 I found I needed to specify a locale like: C:\www\home\websites\mysource_matrix>c:\PHP\php.exe install\compile_locale.php c:\www\home\websites\mysource_matrix --locale=en.

Apache (config for Matrix): a virtual host needs to be created, which for my setup of Apache is in conf/extra/httpd-vhosts.conf. I created a named virtual host for Matrix with the lines:

  NameVirtualHost site1.local
  NameVirtualHost 127.0.0.1

(apparently using localhost won't be sufficient).

The installation directories are a matter of personal preference, but as I could see some long directory paths, I've set the Matrix Home directory to C:/www/home/. This allows a fairly close following of the suggested config for UNIX, though file paths still need to be edited to cater for Windows directories. The relevant virtual container starts:

<VirtualHost 127.0.0.1>
 ServerName site1.local
 DocumentRoot "C:/www/home/websites/mysource_matrix/core/web"
 Options -Indexes FollowSymLinks

I also found that I needed to insert another alias into the Apache httpd.conf for asset_types: Alias /asset_types "C:/www/home/websites/mysource_matrix/data/public/asset_types" Alias / "C:/www/home/websites/mysource_matrix/core/web/index.php/"

I then followed a quick start guide and was able to complete the steps there.

Conclusion

Not a 5 minute install like WordPress, but it is fairly straightforward, at least in hindsight!